UnrestrictedBoundedHomotopy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Whole-union boundary invariance without uniform homotopy speeds

Finite subdivisions are chosen separately on each component. The two sums of consecutive samples have uniformly close localized operators. Rotation and direct-sum additivity cancel the common interior samples in actual Roe K₁.

theorem OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.sampled_telescope line 23
theorem OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.endpoint_boundary_eq line 44

theorem OAI.CoarseAssembly.Rips.ampleRipsFamilyBoundary_boundedHomotopy line 61

Source documentation

Arbitrary componentwise continuous unital self-adjoint homotopies with a common operator bound preserve the whole-union Roe boundary.

theorem ampleRipsFamilyBoundary_boundedHomotopy
    (o : ∀ i, Q i) (hr : 0 ≤ r)
    (χ : ∀ i, C(Point (Q i) r, ℂ) →⋆ₐ[ℂ] ℂ)
    (h : ∀ i, OddHomotopy C(Point (Q i) r, ℂ))
    (hπ : ∀ t i, (h i).representation t 1 = 1)
    (hs : ∀ t i, IsSelfAdjoint ((h i).operator t))
    (C : ℝ) (hC : 1 ≤ C) (hn : ∀ t i, ‖(h i).operator t‖ ≤ C) :
    letI := separatedMetric o
…

Mentions: OAI.CoarseAssembly.Rips.Point, OAI.CoarseAssembly.separatedMetric