OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBasepointFactorCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.basepoint_factor_cover line 31

   Source documentation

   Converting the two adjoint image inclusions to the actual factor change gives both the density-cover condition and the suffix support.

   theorem basepoint_factor_cover
       (hφ : ∀ h : H, F.action (F.ExpD (F.D.equiv h)) =
         M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN hbijN dynkinN h)
       {K : ℝ} (hLip : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
       (A C B D : Set F.N.carrier) {RH HT : ℝ}
       (hbound : ∀ h : H, ‖(finBasis ℝ H).equivFun h‖ ≤ RH →
         ‖eW (heightProjection T.character (h : GroupLieAlgebra (𝓘(ℝ, EG)) G))‖ ≤ HT →
         (M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN hbijN dynkinN h '' A ⊆ C) ∧
         (M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN hbijN dynkinN h '' B ⊆ D))
       (hprod : ∀ x ∈ C, ∀ u ∈ C, ∀ a ∈ C, x⁻¹ * u⁻¹ * a ∈ B)
       (g : G) (u : F.N.carrier) (k : F.D.carrier) (h : H)
       (he : F.ExpD (F.D.equiv h) = k)
   …

   Mentions: OAI.PolycyclicRecognition.heightProjection