OAI/Topology/CoarseAssembly/RipsPathCoarsening.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coarsening preserves the parametrized graph loop

The paths at different Rips scales are the same barycentric paths. This gives equality of their pushed-forward analytic classes, not merely a choice of unrelated loops at successive scales.

  1. theorem OAI.CoarseAssembly.Rips.coarsen_interpolate line 19
  2. theorem OAI.CoarseAssembly.Rips.coarsen_edgePath line 26
  3. theorem OAI.CoarseAssembly.Rips.coarsen_walkPath line 31
  4. theorem OAI.CoarseAssembly.Rips.coarsen_loopCircle line 46