CartanConjugationBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform box bounds for the actual residual Cartan action

The finitely many letter-root bounds give one polynomial in the Cartan coordinate norm. Propagating this through bracket words gives the residual part of the box-conjugation estimate, without an assumed operator bound.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_residual_letter_bound line 24

Source documentation

A polynomial bound on one letter, uniform over the finite word bases.

theorem exists_residual_letter_bound (i : Fin M.letterCount) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (β : M.Bases) (h : H),
      ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (cartanIdealResidualAutomorphism T H h (M.letter i))‖ ≤
      C * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^
        finrank ℝ (rootSpace H (M.weight i)) := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_residual_letters_bound line 42

Source documentation

One polynomial simultaneously bounds every letter image in every unscaled word basis.

theorem exists_residual_letters_bound :
    ∃ (C : ℝ) (p : ℕ), 0 ≤ C ∧ ∀ (β : M.Bases) (h : H) (i : Fin M.letterCount),
      ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (cartanIdealResidualAutomorphism T H h (M.letter i))‖ ≤
      C * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_residual_box_bound line 67

Source documentation

The actual residual action has a uniform polynomial bound in every maximizing scaled word box.

theorem exists_residual_box_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 →
      ∀ r : ℝ, 0 ≤ r → ∀ (h : H) (v : cartanRootIdeal H),
      ‖(M.boxBasis T hunimod eW E β r).equivFun (cartanIdealResidualAutomorphism T H h v)‖ ≤
        A * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p *
          ‖(M.boxBasis T hunimod eW E β r).equivFun v‖ := by
…

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