NormalizedPairInverseLabels.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Inverse coefficients for the actual normalized quasi-inverse pairs

theorem OAI.PolycyclicRecognition.CartanFactorModel.normalized_pair_inverse_coefficients line 25

Source documentation

The inverse normalization only left-translates the inverse map, which cancels in two-point height differences. Thus the proved sublinear labels of the normalized pairs are genuinely inverse coefficients.

theorem normalized_pair_inverse_coefficients
    (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).comp (A p) = ContinuousLinearMap.id ℝ W := by
…

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