OAI/GroupTheory/PolycyclicRecognition/Geometry/FacetRootSwitch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Co-location of neighboring sheets at a contact facet

  1. theorem OAI.PolycyclicRecognition.facet_root_switch_sublinear line 20

    Source documentation

    Vanishing enlargement of the allowed generator amplitude is absorbed at the exact facet height. The estimate is uniform in every initial sheet.

    theorem facet_root_switch_sublinear
    {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