OAI/Topology/CoarseAssembly/FilledEdges.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoarseAssembly.realLatticeRadius_add_le line 17
2. def OAI.CoarseAssembly.realVertex line 28
3. theorem OAI.CoarseAssembly.realLatticeRadius_vertex line 30
4. def OAI.CoarseAssembly.filledVertex line 36
5. def OAI.CoarseAssembly.filledSegment line 39
6. theorem OAI.CoarseAssembly.filledSegment_val line 55
7. theorem OAI.CoarseAssembly.latticeHat_vertex line 58
8. theorem OAI.CoarseAssembly.filledToRips_vertex line 75
9. theorem OAI.CoarseAssembly.realLatticeRadius_adj_difference line 90
10. theorem OAI.CoarseAssembly.latticeHat_eq_radius line 119
11. theorem OAI.CoarseAssembly.filledSegment_hat_left line 122
12. theorem OAI.CoarseAssembly.filledSegment_hat_right line 133
13. theorem OAI.CoarseAssembly.Rips.Point.weight_zero_of_two line 146
14. theorem OAI.CoarseAssembly.filledToRips_edge line 160

    Source documentation

    The actual hat-function filling agrees exactly with the Rips edge.

    theorem filledToRips_edge {j : ℕ} {u v : Disc j} (h : (discGraph j).Adj u v)
        (t : unitInterval) :
        filledToRipsPoint j (filledSegment (filledVertex u) (filledVertex v) t) =
          edgePath (show dist u v ≤ (1 : ℝ) by
            rw [discGraphMetric_eq]
            change ((discGraph j).dist u v : ℝ) ≤ 1
            exact_mod_cast (show (discGraph j).dist u v ≤ 1 by
              simpa using (discGraph j).dist_le h.toWalk)) t := by
    …

    Mentions: OAI.CoarseAssembly.Disc, OAI.CoarseAssembly.discGraph, OAI.CoarseAssembly.filledToRipsPoint, OAI.CoarseAssembly.filledSegment, OAI.CoarseAssembly.filledVertex, OAI.CoarseAssembly.discGraphMetric_eq