PairHeightCocycle.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

+# Height evaluation on the compact pair space

The normalized action makes evaluation of a continuous height homomorphism an actual continuous L² cocycle. The stationary slope estimate therefore applies to this concrete cocycle.

def OAI.PolycyclicRecognition.pairHeight line 26
Source documentation
Height evaluation of the forward map of a normalized pair.
```
def pairHeight (π : G →* Multiplicative W) (g : G) (p : NormalizedPair G Λ) : W :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
theorem OAI.PolycyclicRecognition.pairHeight_cocycle line 30
theorem OAI.PolycyclicRecognition.continuous_pairHeight line 39
def OAI.PolycyclicRecognition.pairHeightProfile line 46
Source documentation
The continuous height profile at a fixed group element.
```
def pairHeightProfile (π : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (g : G) : C(NormalizedPair G Λ, W) :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
theorem OAI.PolycyclicRecognition.continuous_pairHeightProfile line 52
def OAI.PolycyclicRecognition.pairHeightL2 line 62
Source documentation
The L² class of height evaluation, using the canonical continuous-map inclusion.
```
def pairHeightL2 (π : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (g : G) : Lp W 2 μ :=
…
```
theorem OAI.PolycyclicRecognition.continuous_pairHeightL2 line 67
theorem OAI.PolycyclicRecognition.isCocycle_pairHeightL2 line 75

theorem OAI.PolycyclicRecognition.normalizedPair_stationary_sublinear line 99

Source documentation

The manuscript's fixed-ergodic-measure slope, now for the actual compact space of normalized pairs and its actual evaluation cocycle.

theorem normalizedPair_stationary_sublinear
    {G W : Type*} [Group G] [MetricSpace G] [ProperSpace G]
    [IsTopologicalGroup G] [IsIsometricSMul G G]
    [NormedAddCommGroup W] [InnerProductSpace ℝ W] [CompleteSpace W]
    [SecondCountableTopology W] {Λ : ℝ≥0}
    [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    [ErgodicSMul G (NormalizedPair G Λ) μ] [μ.InnerRegularCompactLTTop]
    (hvan : ReducedCohomologyInput G (ZeroMeanL2 (W := W) μ))
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.ReducedCohomologyInput, OAI.PolycyclicRecognition.ZeroMeanL2