OAI/Topology/CoarseAssembly/RipsPaths.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Paths in a finite Rips realization

Straight barycentric interpolation in a simplex, including its endpoint and cocycle-lift formulas. These are paths in the actual realization.+

  1. theorem OAI.CoarseAssembly.Rips.vertex_weight line 21
  2. def OAI.CoarseAssembly.Rips.interpolate line 24
  3. theorem OAI.CoarseAssembly.Rips.interpolate_continuous line 50
  4. theorem OAI.CoarseAssembly.Rips.interpolate_zero line 58
  5. theorem OAI.CoarseAssembly.Rips.interpolate_one line 63
  6. def OAI.CoarseAssembly.Rips.simplexPath line 68
  7. def OAI.CoarseAssembly.Rips.edgePath line 75
  8. theorem OAI.CoarseAssembly.Rips.IntegralCocycle.charge_self line 86
  9. theorem OAI.CoarseAssembly.Rips.IntegralCocycle.localAngle_vertex line 91
  10. theorem OAI.CoarseAssembly.Rips.IntegralCocycle.circleMap_vertex line 96
  11. theorem OAI.CoarseAssembly.Rips.IntegralCocycle.localAngle_interpolate line 101
  12. theorem OAI.CoarseAssembly.Rips.IntegralCocycle.circleMap_edgePath line 109

    Source documentation

    The edge has the real lift t ↦ t * charge x y.

    theorem IntegralCocycle.circleMap_edgePath (c : IntegralCocycle X r)
    {x y : X} (hxy : dist x y ≤ r) (t : unitInterval) :
    c.circleMap (edgePath hxy t) = ((t : ℝ) * (c.charge x y : ℝ) : ℝ) := by
…

    Mentions: OAI.CoarseAssembly.Rips.IntegralCocycle, OAI.CoarseAssembly.Rips.edgePath