CartanBoxMaps.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Propagating root-action bounds through Cartan boxes

A Lie map which preserves the letter root spaces has a polynomial bound in every maximizing box. The proof propagates the bounds on letters through actual bracket words, then through their coordinate basis. This is the algebraic step in the box-conjugation estimate.

theorem OAI.PolycyclicRecognition.evalBracketWord_exp_smul line 25
Source documentation
Independent exponential scaling of letters multiplies a word by the exponential of the sum of its letter exponents.
```
theorem evalBracketWord_exp_smul (X : I → L) (s : I → ℝ) (r : ℝ) (w : FreeMagma I) :
    evalBracketWord (fun i => Real.exp (r * s i) • X i) w =
      Real.exp (r * bracketWordExponent s w) • evalBracketWord X w := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.norm_basis_linearMap_le line 38

Source documentation

A bound on the images of basis vectors bounds the full linear map in the coordinate maximum norm.

theorem norm_basis_linearMap_le {J : Type*} [Fintype J] (b : Basis J ℝ L)
    (F : L →ₗ[ℝ] L) {K : ℝ}
    (hF : ∀ j, ‖b.equivFun (F (b j))‖ ≤ K) (v : L) :
    ‖b.equivFun (F v)‖ ≤ (Fintype.card J : ℝ) * K * ‖b.equivFun v‖ := by
…

theorem OAI.PolycyclicRecognition.image_exponentialCoordinateBox_subset line 57

Source documentation

A coordinate bound transfers to the exponential image when the maps intertwine the exponential.

theorem image_exponentialCoordinateBox_subset
    {G J : Type*} [Fintype J] (b : Basis J ℝ L) (Exp : L → G)
    (F : L →ₗ[ℝ] L) (f : G → G) (hcomm : ∀ x, f (Exp x) = Exp (F x))
    {A : ℝ} (hA : 0 ≤ A) (hF : ∀ x, ‖b.equivFun (F x)‖ ≤ A * ‖b.equivFun x‖)
    (R : ℝ) : f '' exponentialCoordinateBox Exp b R ⊆ exponentialCoordinateBox Exp b (A * R) := by
…

Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox

def OAI.PolycyclicRecognition.CartanWordModel.wordDegreeBound line 75
Source documentation
A fixed degree bound for the finite list of actual words.
```
def wordDegreeBound : ℕ := ∑ w : M.wordList, bracketWordLength (w : FreeMagma (Fin M.letterCount))
…
```
Mentions: OAI.PolycyclicRecognition.bracketWordLength
theorem OAI.PolycyclicRecognition.CartanWordModel.word_degrees_le line 78

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_box_lieMap_bound line 88

Source documentation

Root-space preservation and a bound on the unscaled letter images imply a uniform polynomial bound on a Lie map in every maximizing scaled box.

theorem exists_box_lieMap_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ β : M.Bases,
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ (F : cartanRootIdeal H →ₗ⁅ℝ⁆ cartanRootIdeal H)
        (K : ℝ), 0 ≤ K →
      (∀ i, (F (M.letter i) : L) ∈ LieAlgebra.rootSpace H (M.weight i)) →
      (∀ i, ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (F (M.letter i))‖ ≤ K) →
      ∀ v, ‖(M.boxBasis T hunimod eW E β r).equivFun (F v)‖ ≤
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_groupBox_automorphism_bound line 159

Source documentation

The Lie-map estimate gives a bound on the actual nilpotent group boxes, using the already constructed group automorphism.

theorem exists_groupBox_automorphism_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ β : M.Bases,
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ (F : cartanRootIdeal H ≃ₗ⁅ℝ⁆ cartanRootIdeal H)
        (K : ℝ), 0 ≤ K →
      (∀ i, (F (M.letter i) : L) ∈ LieAlgebra.rootSpace H (M.weight i)) →
      (∀ i, ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (F (M.letter i))‖ ≤ K) →
      ∀ R : ℝ,
…