CartanRootWidths.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Root-space widths inside actual word boxes

A nonzero coordinate of a root vector can occur only at a word of the same weight. Its word exponent dominates the support of that root. Consequently rescaling a letter-root vector never enlarges its coordinates in the scaled word box. This includes zero-weight bracket directions.

theorem OAI.PolycyclicRecognition.basis_repr_map_of_diagonal line 20

theorem OAI.PolycyclicRecognition.CartanWordModel.wordWeight_eq_of_repr_ne_zero line 44

Source documentation

A root vector has nonzero word coordinates only in its own weight.

theorem wordWeight_eq_of_repr_ne_zero (β : M.Bases) (χ : Weight ℝ H L)
    (v : cartanRootIdeal H) (hv : (v : L) ∈ rootSpace H χ)
    (j : Fin (finrank ℝ (cartanRootIdeal H)))
    (hj : (WordBasisSelections.basis M.letter M.wordList β).repr v j ≠ 0) (h : H) :
    bracketWordExponent (fun i => M.weight i h) (β.val j) = χ h := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.CartanWordModel.letter_support_le_wordCost line 72

Source documentation

The exponent of a word of a letter's weight is at least that letter's support, since separate letter supports dominate evaluation at one point.

theorem letter_support_le_wordCost {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (i : Fin M.letterCount) (z : M.wordList)
    (hz : ∀ h : H, bracketWordExponent (fun k => M.weight k h) z = M.weight i h) :
    (M.supportIn T hunimod eW).weightSupport E i ≤ M.boxCost T hunimod eW E z := by
…

Mentions: OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.CartanWordModel.letter_support_le_wordCost_of_repr_ne_zero line 87

Source documentation

Nonzero coordinates of an arbitrary vector in a letter's root space occur only at word exponents dominating that letter's support.

theorem letter_support_le_wordCost_of_repr_ne_zero
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) (β : M.Bases)
    (i : Fin M.letterCount) (v : cartanRootIdeal H)
    (hv : (v : L) ∈ rootSpace H (M.weight i))
    (j : Fin (finrank ℝ (cartanRootIdeal H)))
    (hj : (WordBasisSelections.basis M.letter M.wordList β).repr v j ≠ 0) :
    (M.supportIn T hunimod eW).weightSupport E i ≤ M.boxCost T hunimod eW E (β.val j) :=
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.CartanWordModel.norm_scaled_root_le line 99

Source documentation

The normalized coordinates of a letter-root vector are bounded by its unscaled coordinates, uniformly over templates and scales.

theorem norm_scaled_root_le {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (β : M.Bases) (i : Fin M.letterCount) (v : cartanRootIdeal H)
    (hv : (v : L) ∈ rootSpace H (M.weight i)) {r : ℝ} (hr : 0 ≤ r) :
    ‖(M.boxBasis T hunimod eW E β r).equivFun
      (Real.exp (r * (M.supportIn T hunimod eW).weightSupport E i) • v)‖ ≤
        ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections.basis

def OAI.PolycyclicRecognition.CartanWordModel.rootInIdeal line 135
Source documentation
Inclusion of a nonzero generalized root space into the Cartan ideal.
```
def rootInIdeal (χ : LieModule.Weight ℝ H L) (hχ : χ.IsNonZero) :
    LieAlgebra.rootSpace H χ →ₗ[ℝ] cartanRootIdeal H where
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_root_wordBasis_bound line 144

Source documentation

The finitely many unscaled word bases have one common comparison constant with fixed coordinates on a nonzero root space.

theorem exists_root_wordBasis_bound (χ : LieModule.Weight ℝ H L) (hχ : χ.IsNonZero) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (β : M.Bases) (v : LieAlgebra.rootSpace H χ),
      ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (rootInIdeal χ hχ v)‖ ≤
      C * ‖(Module.finBasis ℝ (LieAlgebra.rootSpace H χ)).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.CartanWordModel.rootInIdeal