OAI/GroupTheory/PolycyclicRecognition/Geometry/RootSupportSwitch.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Logarithmically short switches at supporting positions

A linearly bounded Cartan position and a bounded contracted amplitude give a switch of length O(log (2 + r)). The constants are independent of the translated sheet and the particular supporting position.

  1. theorem OAI.PolycyclicRecognition.logarithmic_root_support_switch_polynomial_position line 26

    Source documentation

    The root-switch estimate in the exact support regime. The hypothesis on the contracted amplitude is satisfied by |t| ≤ B exp (χ h).

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

  2. theorem OAI.PolycyclicRecognition.logarithmic_root_support_switch line 77

    Source documentation

    In particular the same estimate holds for linearly bounded Cartan logarithms, as in a single support leg.

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