ProfileHeightIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact height increments of sampled profiles

theorem OAI.PolycyclicRecognition.pairHeight_chartOccupationPoint line 21
Source documentation
Normalization at a chart point subtracts exactly its starting height.
```
theorem pairHeight_chartOccupationPoint (π : G →* Multiplicative W)
    (p : NormalizedPair G Λ) (x a k y d : G) :
    pairHeight π d (chartOccupationPoint p x a k y) =
      (π (p.val.1 (x * a * k * y * d))).toAdd -
        (π (p.val.1 (x * a * k * y))).toAdd := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight, OAI.PolycyclicRecognition.chartOccupationPoint

theorem OAI.PolycyclicRecognition.rescaledMapProfile_increment_eq_pairHeight line 35

Source documentation

The increment along the actual scaled path is the normalized pair cocycle, with the same total time used in the microstep estimate.

theorem rescaledMapProfile_increment_eq_pairHeight
    (π : G →* Multiplicative W) (p : NormalizedPair G Λ)
    (x a k : G) (r T : ℝ) (φ : Z → G) (z w : Z) (d : G)
    (hend : φ w = φ z * d) :
    T⁻¹ • (rescaledMapProfile (fun g => (π (p.val.1 g)).toAdd) x (a * k) r φ w -
      rescaledMapProfile (fun g => (π (p.val.1 g)).toAdd) x (a * k) r φ z) =
      (Real.exp r * T)⁻¹ • pairHeight π d (chartOccupationPoint p x a k (φ z)) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.rescaledMapProfile, OAI.PolycyclicRecognition.pairHeight, OAI.PolycyclicRecognition.chartOccupationPoint