OAI/GroupTheory/PolycyclicRecognition/Algebra/FacetPivotBridgeRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A vanishing rate for the actual bridge at the facet pivot

  1. theorem OAI.PolycyclicRecognition.distance_rate_tendsto_zero line 14
  2. theorem OAI.PolycyclicRecognition.exists_facet_pivot_bridge_rate line 32

    Source documentation

    No bridge estimate is postulated: root distortion at the exact facet height supplies a nonnegative error rate tending to zero, uniformly over the initial source state.

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