OAI/Topology/CoarseAssembly/RipsWindingTest.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Winding tests from the short-loop theorem

This connects the proved graph-theoretic small-loop argument to the actual continuous circle map and its real path lift. It assumes no analytic pairing or nonvanishing conclusion.

  1. def OAI.CoarseAssembly.graphRipsCocycle line 22
  2. theorem OAI.CoarseAssembly.graphRipsCocycle_on_walk line 44
  3. theorem OAI.CoarseAssembly.graph_winding_lift line 55

    Source documentation

    The winding test on a finite Rips component has a real lift with the same endpoint as the original graph charge.

    theorem graph_winding_lift [Fintype X] (hG : G.Connected) (a : X → X → ℤ)
    (ha : ∀ x y, G.Adj x y → a y x = -a x y) (r : ℕ) (hr : 1 ≤ r)
    (hloop : ∀ x (p : G.Walk x x), p.length ≤ 3 * r → walkCharge a p = 0)
    {x : X} (p : G.Walk x x) :
    letI := graphMetric G hG
…

    Mentions: OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.graphMetric