NormalizedPairBackwardHeight.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform height estimates for the actual backward maps

theorem OAI.PolycyclicRecognition.CartanFactorModel.normalized_pair_inverse_equiv line 23

Source documentation

The already proved inverse-coefficient identity determines the inverse linear equivalence, including the normalization translation.

theorem normalized_pair_inverse_equiv
    (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)
    {Λ : ℝ≥0} (A : NormalizedPair G Λ → W ≃L[ℝ] W)
    {K : ℝ} (hK : 0 ≤ K)
    (hπ : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ p x y,
      ‖(π (p.val.1 y)).toAdd - (π (p.val.1 x)).toAdd - A p ((π (x⁻¹ * y)).toAdd)‖ ≤
        ε * dist x y + D) (p : NormalizedPair G Λ) :
    A (pairChartTransition (1, p)).1 = (A p).symm := by
…

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

theorem OAI.PolycyclicRecognition.CartanFactorModel.normalized_pair_backward_sublinear_height line 45

Source documentation

The backward maps inherit the same uniform two-point error, with the inverse coefficient. Left normalization cancels exactly in their heights.

theorem normalized_pair_backward_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)
    {Λ : ℝ≥0} (A : NormalizedPair G Λ → W ≃L[ℝ] W)
    {K : ℝ} (hK : 0 ≤ K)
    (hπ : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ p x y,
      ‖(π (p.val.1 y)).toAdd - (π (p.val.1 x)).toAdd - A p ((π (x⁻¹ * y)).toAdd)‖ ≤
        ε * dist x y + D) :
    ∀ ε : ℝ, 0 < ε → ∃ D : ℝ, 0 ≤ D ∧ ∀ p x y,
…

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