ContinuousFlowDistortion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous contracting flows

The local metric bounds in logarithmic distortion follow from continuity and compactness. A continuous one-parameter homomorphism has at most linear metric growth, so no differentiability estimate needs to be assumed here.

theorem OAI.PolycyclicRecognition.dist_one_pow_le line 22
theorem OAI.PolycyclicRecognition.continuous_flow_linear_growth line 34
Source documentation
Every continuous one-parameter homomorphism has a linear metric bound for times at least one, using only boundedness of its compact unit interval.
```
theorem continuous_flow_linear_growth
    (d : ℝ → G) (hd : Continuous d) (hd0 : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t) :
    ∃ L : ℝ, 0 ≤ L ∧ ∀ t, 1 ≤ t → dist 1 (d t) ≤ L * t := by
…
```

theorem OAI.PolycyclicRecognition.logarithmic_distortion_of_continuous_flow line 69

Source documentation

For a continuous exponential chart and continuous contracting flow, polynomially corrected contraction implies an actual logarithmic distance bound. The compact unit-ball bound and the flow-length bound are derived in the proof.

theorem logarithmic_distortion_of_continuous_flow
    {V : Type*} [NormedAddCommGroup V] [ProperSpace V]
    (Exp : V → G) (hExp : Continuous Exp)
    (d : ℝ → G) (hd : Continuous d) (hd0 : d 0 = 1)
    (hmul : ∀ s t, d (s + t) = d s * d t) (T : ℝ → V → V)
    {C : ℝ} (hC : 0 ≤ C) (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‖) :
    ∃ D : ℝ, 0 < D ∧ ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + ‖v‖) := by
…