CartanControlledProducts.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for products of controlled Cartan increments

Each increment begins in a fixed nilpotent coordinate box. Its Cartan height lies in a scaled template, and its Cartan logarithm has a polynomial bound. The resulting product remains in the template box with polynomial radius. All constants are uniform over templates, maximizing bases and scales.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_controlled_adjoint_group_bound line 34

Source documentation

A controlled Cartan action takes an unscaled box into the template box.

theorem exists_controlled_adjoint_group_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ (A : ℝ) (p : ℕ), 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 →
      ∀ (γ : M.Bases) (r : ℝ), 0 ≤ r → ∀ (h : H) (w : W), w ∈ E →
      eW (heightProjection T.character (h : L)) = r • w → ∀ (R : ℝ) (g : N),
      g ∈ exponentialCoordinateBox (Exp ∘ eN)
        (WordBasisSelections.basis M.letter M.wordList γ) R →
      M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h g ∈
        M.groupBox T hunimod eW (Exp ∘ eN) E β r
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_controlled_product_bound line 59

Source documentation

Polynomial Cartan logarithms give a polynomial radius for the full product, even when the height template and scale vary.

theorem exists_controlled_product_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {B R : ℝ} (hB : 0 ≤ B) (hR : 0 ≤ R) (k : ℕ) :
    ∃ (C : ℝ) (q : ℕ), 0 ≤ C ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ β : M.Bases,
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ (γ : M.Bases) (r : ℝ), 0 ≤ r → ∀ (m : ℕ) (h : Fin m → H) (w : Fin m → W),
      (∀ i, w i ∈ E) →
      (∀ i, eW (heightProjection T.character (h i : L)) = r • w i) →
      (∀ i, ‖(Module.finBasis ℝ H).equivFun (h i)‖ ≤ B * (1 + (m : ℝ)) ^ k) →
      ∀ g : Fin m → N,
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.heightProjection