CartanRootBoxes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Generator steps lie in the actual enlarged Cartan boxes

theorem OAI.PolycyclicRecognition.CartanWordModel.letter_step_mem_groupBox line 22

Source documentation

A generator interval of its support width fits the word box. The only constant is the generator's coordinate norm in the unscaled word basis.

theorem letter_step_mem_groupBox {N : Type*} (Exp : cartanRootIdeal H → N)
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) (β : M.Bases)
    (i : Fin M.letterCount) {r R t : ℝ} (hr : 0 ≤ r)
    (ht : |t| ≤ R * Real.exp (r * (M.supportIn T hunimod eW).weightSupport E i)) :
    Exp (t • M.letter i) ∈ M.groupBox T hunimod eW Exp E β r
      (R * ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun (M.letter i)‖) := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_letter_groupBox_bound line 43

Source documentation

One constant works for every generator and every selected word basis, independently of the template and the physical scale.

theorem exists_uniform_letter_groupBox_bound {N : Type*} (Exp : cartanRootIdeal H → N) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (E : Set W), IsCompact E → E.Nonempty →
      ∀ (β : M.Bases) (i : Fin M.letterCount) (r R t : ℝ), 0 ≤ r → 0 ≤ R →
      |t| ≤ R * Real.exp (r * (M.supportIn T hunimod eW).weightSupport E i) →
      Exp (t • M.letter i) ∈ M.groupBox T hunimod eW Exp E β r (R * C) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal