CartanInverseCoefficients.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Coarse inverses have inverse linear height coefficients

theorem OAI.PolycyclicRecognition.CartanFactorModel.inverse_coefficients_of_sublinear_height line 24

Source documentation

Comparing the composition to the identity on the actual Cartan height rays identifies the coefficients. No inverse relation is assumed.

theorem inverse_coefficients_of_sublinear_height
    (eW : HeightSpace T.character ≃ₗ[ℝ] W) (π : G →* Multiplicative W)
    (hπExp : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
    (chartD : GroupLieAlgebra (𝓘(ℝ, F.D.modelSpace)) F.D.carrier ≃ₜ F.D.carrier)
    (hchartD : ∀ x, chartD x = F.ExpD x)
    (f g : G → G) (A B : W →L[ℝ] W)
    {K L C D : ℝ} (hK : 0 ≤ K) (hL : 0 ≤ L) (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hπ : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
    (hfLip : ∀ x y, dist (f x) (f y) ≤ L * dist x y + C)
    (hinv : ∀ x, dist (g (f x)) x ≤ D)
    (hf : ∀ ε : ℝ, 0 < ε → ∃ E : ℝ, 0 ≤ E ∧ ∀ x y,
      ‖(π (f y)).toAdd - (π (f x)).toAdd - A ((π y).toAdd - (π x).toAdd)‖ ≤
…

Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection