LogDistortion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic distortion from polynomially corrected contraction

The nilpotent part of a real weight action introduces a polynomial factor. It is absorbed by an additional logarithmic conjugating time. These lemmas retain that factor instead of assuming a semisimple action.

theorem OAI.PolycyclicRecognition.exists_logarithmic_contraction_time line 23
Source documentation
A polynomial correction to exponential contraction can be absorbed uniformly at a time bounded by twice the logarithm of the initial size.
```
theorem exists_logarithmic_contraction_time {C : ℝ} (hC : 0 ≤ C) (b : ℕ) :
    ∃ a : ℝ, 0 ≤ a ∧ ∀ R : ℝ, 0 ≤ R →
      let t := 2 * Real.log (2 + R) + a
…
```
theorem OAI.PolycyclicRecognition.dist_one_mul_le line 84
Source documentation
Product lengths in a left invariant metric.
```
theorem dist_one_mul_le (a b : G) : dist 1 (a * b) ≤ dist 1 a + dist 1 b := by
…
```
theorem OAI.PolycyclicRecognition.dist_one_conjugate_le line 90
Source documentation
Conjugation costs at most twice the conjugating length.
```
theorem dist_one_conjugate_le (a x : G) :
    dist 1 (a * x * a⁻¹) ≤ 2 * dist 1 a + dist 1 x := by
…
```

theorem OAI.PolycyclicRecognition.logarithmic_distortion_of_contracting_flow line 101

Source documentation

Exponential contraction up to a polynomial, together with a bounded unit neighborhood and linear conjugating paths, implies logarithmic distortion.

theorem logarithmic_distortion_of_contracting_flow
    {V : Type*} [NormedAddCommGroup V]
    (Exp : V → G) (d : ℝ → G) (T : ℝ → V → V)
    {C L B : ℝ} (hC : 0 ≤ C) (hL : 0 ≤ L) (hB : 0 ≤ B) (b : ℕ)
    (hconj : ∀ v t, 0 ≤ t → Exp v = d t * Exp (T t v) * (d t)⁻¹)
    (hcontract : ∀ v t, 0 ≤ t → ‖T t v‖ ≤ C * (1 + t) ^ b * Real.exp (-t) * ‖v‖)
    (hpath : ∀ t, 1 ≤ t → dist 1 (d t) ≤ L * t)
    (hlocal : ∀ v, ‖v‖ ≤ 1 → dist 1 (Exp v) ≤ B) :
    ∃ D : ℝ, 0 < D ∧ ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖) := by
…