CocycleCircleMap.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The circle map of an integral Rips cocycle

On each finite component, barycentric interpolation of an integral edge cocycle defines a genuine continuous map to ℝ / ℤ. The local real lifts differ by the integral edge charge. This constructs the winding test in the manuscript, rather than assuming its topological extension.

structure OAI.CoarseAssembly.Rips.IntegralCocycle line 26
Source documentation
Integral charges with the two identities required on a Rips simplex.
```
structure IntegralCocycle (X : Type*) [PseudoMetricSpace X] (r : ℝ) where
…
```
theorem OAI.CoarseAssembly.Rips.IntegralCocycle.difference line 32
theorem OAI.CoarseAssembly.Rips.Point.exists_positive line 39
def OAI.CoarseAssembly.Rips.Point.supportVertex line 48
theorem OAI.CoarseAssembly.Rips.Point.supportVertex_positive line 50
theorem OAI.CoarseAssembly.Rips.Point.supportVertex_mem line 53
def OAI.CoarseAssembly.Rips.IntegralCocycle.localAngle line 60
Source documentation
Local real lift based at a vertex of the supporting simplex.
```
def IntegralCocycle.localAngle (c : IntegralCocycle X r) (x : X) (p : Point X r) : ℝ :=
…
```
Mentions: OAI.CoarseAssembly.Rips.IntegralCocycle, OAI.CoarseAssembly.Rips.Point
theorem OAI.CoarseAssembly.Rips.IntegralCocycle.localAngle_continuous line 63
theorem OAI.CoarseAssembly.Rips.Point.sum_weight line 68
theorem OAI.CoarseAssembly.Rips.IntegralCocycle.localAngle_sub line 73
Source documentation
Changes of local lift are exactly the prescribed integral charges.
```
theorem IntegralCocycle.localAngle_sub (c : IntegralCocycle X r) (p : Point X r)
    {x y : X} (hx : x ∈ p.weight.support) (hy : y ∈ p.weight.support) :
    c.localAngle x p - c.localAngle y p = (c.charge x y : ℝ) := by
…
```
Mentions: OAI.CoarseAssembly.Rips.IntegralCocycle, OAI.CoarseAssembly.Rips.Point
theorem OAI.CoarseAssembly.Rips.IntegralCocycle.localAngle_coe_eq line 94
def OAI.CoarseAssembly.Rips.IntegralCocycle.circleMap line 103
Source documentation
Barycentric interpolation of the cocycle, with values in the unit circle.
```
def IntegralCocycle.circleMap (c : IntegralCocycle X r) (p : Point X r) :
    AddCircle (1 : ℝ) := c.localAngle p.supportVertex p
```
Mentions: OAI.CoarseAssembly.Rips.IntegralCocycle, OAI.CoarseAssembly.Rips.Point
theorem OAI.CoarseAssembly.Rips.IntegralCocycle.circleMap_eq line 106
theorem OAI.CoarseAssembly.Rips.IntegralCocycle.circleMap_continuous line 111
def OAI.CoarseAssembly.Rips.IntegralCocycle.toContinuousMap line 125