OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanConeIdealExponent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.sum_coneIdealCost_eq_templateSupport line 24

   Source documentation

   If the cone widths vanish, the pure quotient words contribute zero. Completing a maximal ideal basis therefore gives exactly P(E).

   theorem sum_coneIdealCost_eq_templateSupport
       (C : Set (H →ₗ[ℝ] ℝ))
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (E : Set W)
       (hs : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport E i)
       (hz : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C →
         (M.supportIn T hunimod eW).weightSupport E i = 0)
       (β : M.ConeIdealBases C)
       (hβ : M.IsMaximizingConeIdealBasis C bI
         ((M.supportIn T hunimod eW).weightSupport E) β) :
       (∑ j, M.coneIdealWordCost C ((M.supportIn T hunimod eW).weightSupport E) (β.val j)) =
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

2. theorem OAI.PolycyclicRecognition.CartanWordModel.sum_coneIdealCost_image_templateSymmetry line 44

   Source documentation

   The target ideal exponent agrees with the source template exponent under the actual finite template-symmetry label.

   theorem sum_coneIdealCost_image_templateSymmetry [FiniteDimensional ℝ W]
       (C : Set (H →ₗ[ℝ] ℝ))
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (E : Set W) (hE : IsCompact E) (hne : E.Nonempty) (hconv : Convex ℝ E)
       (A : templateSymmetryGroup (M.supportIn T hunimod eW))
       (hs : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport (A.val '' E) i)
       (hz : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C →
         (M.supportIn T hunimod eW).weightSupport (A.val '' E) i = 0)
       (β : M.ConeIdealBases C)
       (hβ : M.IsMaximizingConeIdealBasis C bI
         ((M.supportIn T hunimod eW).weightSupport (A.val '' E)) β) :
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.templateSymmetryGroup