PairMeanControl.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Metric control of the actual stationary mean

The common Lipschitz constant of normalized pairs bounds their height profiles, and hence bounds the homomorphism obtained by integration. Consequently the actual averaged homomorphism kills every root flow.

theorem OAI.PolycyclicRecognition.norm_pairHeight_le line 30
Source documentation
Pointwise height control uses the forward normalization at the identity.
```
theorem norm_pairHeight_le (π : G →* Multiplicative W)
    (hπ : LipschitzWith K (fun g => (π g).toAdd))
    (g : G) (p : NormalizedPair G Λ) :
    ‖pairHeight π g p‖ ≤ (K : ℝ) * Λ * dist 1 g := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight

def OAI.PolycyclicRecognition.normalizedPairMeanSlope line 50

Source documentation

The averaged slope of the actual evaluation cocycle.

def normalizedPairMeanSlope (π : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) : G →* Multiplicative W :=
…

theorem OAI.PolycyclicRecognition.continuous_normalizedPairMeanSlope line 55

theorem OAI.PolycyclicRecognition.norm_normalizedPairMeanSlope_le line 62

Source documentation

Integration preserves the common linear metric bound.

theorem norm_normalizedPairMeanSlope_le (π : G →* Multiplicative W)
    (hπ : LipschitzWith K (fun g => (π g).toAdd)) (g : G) :
    ‖(normalizedPairMeanSlope μ π hπ.continuous g).toAdd‖ ≤
      (K : ℝ) * Λ * dist 1 g := by
…

Mentions: OAI.PolycyclicRecognition.normalizedPairMeanSlope