NormalizedRipsFamily.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Whole-union representatives from arbitrary finite-Rips cycles

Each root gives an evaluation character. The proved unital normalization removes the unitality and uniform operator-bound premises from the raw family construction. Descent through all analytic cycle relations remains a separate obligation.

def OAI.CoarseAssembly.Rips.rootCharacter line 22
def OAI.CoarseAssembly.Rips.normalizedRipsCycle line 31
theorem OAI.CoarseAssembly.Rips.normalizedRipsCycle_properties line 35
def OAI.CoarseAssembly.Rips.normalizedRipsFamilyBoundary line 47
Source documentation
An actual whole-union Roe class for every family of compact-source cycles, with all normalization premises discharged.
```
def normalizedRipsFamilyBoundary (o : ∀ i, V i) (r : ℝ) (hr : 0 ≤ r)
    (c : ∀ i, OddCycle C(Point (V i) r, ℂ)) :
    letI := separatedMetric o
…
```
Mentions: OAI.CoarseAssembly.Rips.Point, OAI.CoarseAssembly.separatedMetric