CartanBoundedHeightEndgame.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded Cartan height from leaf and transversal estimates

Leaf bounds, averaged trace bounds and sublinear height control together give a uniform bound on the height error.

theorem OAI.PolycyclicRecognition.CartanFactorModel.uniform_affine_bound_of_leaf_and_averaged_traces line 29

Source documentation

The actual factorization and Cartan rays finish bounded affine height once the leaf and boundary-trace estimates have been supplied.

theorem uniform_affine_bound_of_leaf_and_averaged_traces
    (height : G →* Multiplicative W)
    (hheight : ∀ x, (height (ExpG x)).toAdd = eW (heightProjection T.character x))
    (hbijN : Function.Bijective F.ExpN)
    (chartD : GroupLieAlgebra (𝓘(ℝ, F.D.modelSpace)) F.D.carrier ≃ₜ F.D.carrier)
    (hchartD : ∀ x, chartD x = F.ExpD x)
    (α β : I → Module.Dual ℝ W)
    (hsep : ∀ w, (∀ i, β i w = 0) → w = 0)
    (η : P → G → W) (A : P → W →ₗ[ℝ] W)
    (hsub : ∀ p ε, 0 < ε → ∃ B : ℝ, ∀ g,
      ‖η p g - η p 1 - A p (height g).toAdd‖ ≤ ε * dist 1 g + B)
    {L B : ℝ} (hL : 0 ≤ L) (hB : 0 ≤ B)
…

Mentions: OAI.PolycyclicRecognition.heightProjection