OAI/Topology/CoarseAssembly/FilledWalks.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Filling the actual parametrized lattice walks

Straight segments in the compact polygon follow the same concatenation as the barycentric graph path. Thus every closed base walk, with its original parametrization, factors through the filled polygon.

  1. theorem OAI.CoarseAssembly.discEdgeBound line 20
  2. def OAI.CoarseAssembly.filledWalk line 27
  3. theorem OAI.CoarseAssembly.filledToRips_walk line 32
  4. theorem OAI.CoarseAssembly.filledToRips_loop line 46

    Source documentation

    Exact factorization through the filled compact polygon, not a homotopy or a change of parametrization.

    theorem filledToRips_loop {j : ℕ} {u : Disc j} (p : (discGraph j).Walk u u) :
    (filledToRips j).comp (loopCircle (filledWalk p)) =
      loopCircle (walkPath (by norm_num : (0 : ℝ) ≤ 1) discEdgeBound p) := by
…

    Mentions: OAI.CoarseAssembly.Disc, OAI.CoarseAssembly.discGraph, OAI.CoarseAssembly.filledToRips, OAI.CoarseAssembly.loopCircle, OAI.CoarseAssembly.filledWalk, OAI.CoarseAssembly.discEdgeBound