PairMicrosteps.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact normalized pair-height microsteps

The inverse power in the normalized left action records the original right translation of the sampling point. The final group remainder is retained.

theorem OAI.PolycyclicRecognition.pairHeight_pow_sum line 25
Source documentation
The actual height cocycle telescopes along successive right microsteps.
```
theorem pairHeight_pow_sum (π : G →* Multiplicative W) (g : G)
    (p : NormalizedPair G Λ) (n : ℕ) :
    pairHeight π (g ^ n) p =
      ∑ j ∈ Finset.range n, pairHeight π g ((g ^ j)⁻¹ • p) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight

theorem OAI.PolycyclicRecognition.pairHeight_pow_mul line 36

Source documentation

Keep the final incomplete step in the telescoping identity.

theorem pairHeight_pow_mul (π : G →* Multiplicative W) (g h : G)
    (p : NormalizedPair G Λ) (n : ℕ) :
    pairHeight π (g ^ n * h) p =
      (∑ j : Fin n, pairHeight π g ((g ^ (j : ℕ))⁻¹ • p)) +
        pairHeight π h ((g ^ n)⁻¹ • p) := by
…

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

theorem OAI.PolycyclicRecognition.normalized_pair_microsteps_convex_bound line 47

Source documentation

The convex distance estimate for the exact microstep decomposition, before bounding the final incomplete step by the Lipschitz constant.

theorem normalized_pair_microsteps_convex_bound
    (π : G →* Multiplicative W) (g h : G) (p : NormalizedPair G Λ)
    (n : ℕ) {L t : ℝ} (hL : 0 < L) (ht : 0 < t) (hn : (n : ℝ) * L ≤ t)
    {S : Set W} (hS : IsCompact S) {w₀ : W} (hw₀ : w₀ ∈ S) :
    infDist (t⁻¹ • pairHeight π (g ^ n * h) p) (convexHull ℝ S) ≤
      (L / t) * (∑ j : Fin n,
        infDist (L⁻¹ • pairHeight π g ((g ^ (j : ℕ))⁻¹ • p)) S) +
      ‖t⁻¹ • pairHeight π h ((g ^ n)⁻¹ • p) - (1 - (n : ℝ) * (L / t)) • w₀‖ := by
…

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

theorem OAI.PolycyclicRecognition.normalized_pair_microsteps_convex_bound_of_remainder line 70

Source documentation

Lipschitz height control makes the incomplete microstep cost at most its relative length times one fixed constant.

theorem normalized_pair_microsteps_convex_bound_of_remainder
    (π : G →* Multiplicative W) (hπ : LipschitzWith K (fun g => (π g).toAdd))
    (g h : G) (p : NormalizedPair G Λ) (n : ℕ)
    {L t D : ℝ} (hL : 0 < L) (ht : 0 < t) (_hD : 0 ≤ D)
    (hn : (n : ℝ) * L ≤ t) (hn' : t ≤ ((n : ℝ) + 1) * L)
    (hrem : dist 1 h ≤ D * L)
    {S : Set W} (hS : IsCompact S) {w₀ : W} (hw₀ : w₀ ∈ S) :
    infDist (t⁻¹ • pairHeight π (g ^ n * h) p) (convexHull ℝ S) ≤
      (L / t) * (∑ j : Fin n,
        infDist (L⁻¹ • pairHeight π g ((g ^ (j : ℕ))⁻¹ • p)) S) +
      (L / t) * ((K : ℝ) * Λ * D + ‖w₀‖) := by
…

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