OAI/GroupTheory/PolycyclicRecognition/Geometry/PublishedRootDistortion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual root distortion from the published linear realization

All contraction, continuity, and conjugation premises of the root-space distortion theorem are now discharged for the ambient Lie group. Only the already recorded faithful exponential-realization input remains assumed.

  1. theorem OAI.PolycyclicRecognition.root_distortion_of_published_realization line 29

    Source documentation

    Every actual nonzero Cartan root space is logarithmically distorted in the ambient metric.

    theorem root_distortion_of_published_realization
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, EG)) G) a)
    (H : LieSubalgebra ℝ (GroupLieAlgebra (𝓘(ℝ, EG)) G)) [H.IsCartanSubalgebra]
    (χ : Weight ℝ H (GroupLieAlgebra (𝓘(ℝ, EG)) G)) (hχ : χ.IsNonZero)
    (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G)) :
…

    Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.ExponentialLinearRealizationInput