LipschitzInversePairBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Lower quasi-isometry bounds from Lipschitz coarse inverses

theorem OAI.PolycyclicRecognition.coarse_lower_of_lipschitz_inverse line 17

Source documentation

A Lipschitz inverse with bounded composition error supplies the lower inequality, with the same enlarged constant used by the compact pair space.

theorem coarse_lower_of_lipschitz_inverse
    {Λ : ℝ≥0} (hΛ : 2 ≤ (Λ : ℝ)) (f : X → Y) (g : Y → X)
    (hg : LipschitzWith Λ g) (hinv : ∀ x, dist (g (f x)) x ≤ Λ) (x y : X) :
    (Λ : ℝ)⁻¹ * dist x y - Λ ≤ dist (f x) (f y) := by
…

theorem OAI.PolycyclicRecognition.lipschitzPairBounds_of_inverse_bounds line 39

Source documentation

No separate lower-bound hypothesis is needed once the two Lipschitz representatives have controlled inverse errors.

theorem lipschitzPairBounds_of_inverse_bounds
    {Λ : ℝ≥0} (hΛ : 2 ≤ (Λ : ℝ)) (p : C(G, G) × C(G, G))
    (hf : LipschitzWith Λ p.1) (hg : LipschitzWith Λ p.2)
    (hgf : ∀ x, dist (p.2 (p.1 x)) x ≤ Λ)
    (hfg : ∀ x, dist (p.1 (p.2 x)) x ≤ Λ) :
    LipschitzPairBounds G Λ p :=
…

Mentions: OAI.PolycyclicRecognition.LipschitzPairBounds