RootSwitchBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Ambient bounds for root switches at a Cartan position

Conjugating a root displacement back from its Cartan position removes its scalar weight, up to the proved polynomial nilpotent correction. Applying actual root distortion gives the logarithmic switch estimate.

theorem OAI.PolycyclicRecognition.dist_right_switch line 25

Source documentation

A switch on a translated right-positioned sheet is measured by its conjugate displacement.

theorem dist_right_switch {G : Type*} [Group G] [PseudoMetricSpace G]
    [IsIsometricSMul G G] (x n d : G) :
    dist (x * d) (x * n * d) = dist 1 (d⁻¹ * n * d) := by
…

theorem OAI.PolycyclicRecognition.root_switch_bound_of_published_realization line 39

Source documentation

The ambient switch estimate, retaining the full nilpotent correction and the exponential scalar contraction at the Cartan position.

theorem root_switch_bound_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