OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCompactSupportSlack.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cartan_height_above_compact_support line 16

   Source documentation

   A compact template inside the open profile domain supplies the strict height slack needed by cartan_interior_neighbor_profiles_eq, for every actual generator weight. The Cartan representative is constructed.

   theorem exists_cartan_height_above_compact_support
       {L W : Type*} [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
       {H : LieSubalgebra ℝ L} [H.IsCartanSubalgebra]
       (M : CartanWordModel H) {n : ℕ} (T : TriangularAdjoint L n)
       (hunimod : ∀ x : L, LinearMap.trace ℝ L (LieAlgebra.ad ℝ L x) = 0)
       (eW : HeightSpace T.character ≃ₗ[ℝ] W)
       (E U : Set W) (hE : IsCompact E) (hEne : E.Nonempty)
       (hU : IsOpen U) (hEU : E ⊆ U) (i : Fin M.letterCount) :
       ∃ h : H, eW (heightProjection T.character (h : L)) ∈ U ∧
         (M.supportIn T hunimod eW).weightSupport E i < M.weight i h := by
   …

   Mentions: OAI.PolycyclicRecognition.CartanWordModel, OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection