CartanControlledAction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cartan actions whose heights stay in a template

The normalized width of a root controls every exponential whose exponent is below that width. Consequently a Cartan action with height in the scaled template sends a fixed coordinate box into the template box with polynomial loss in its Cartan logarithm. This is the increment estimate for controlled paths.

theorem OAI.PolycyclicRecognition.norm_map_between_bases_le line 21

theorem OAI.PolycyclicRecognition.CartanWordModel.norm_scaled_root_le_of_exponent_le line 49

Source documentation

Any smaller root exponent satisfies the normalized width estimate.

theorem norm_scaled_root_le_of_exponent_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 t : ℝ} (hr : 0 ≤ r)
    (ht : t ≤ r * (M.supportIn T hunimod eW).weightSupport E i) :
    ‖(M.boxBasis T hunimod eW E β r).equivFun (Real.exp t • v)‖ ≤
      ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun v‖ := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.norm_adjoint_letter_le line 65

Source documentation

Height containment absorbs the entire scalar part of each letter image.

theorem norm_adjoint_letter_le
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) (β : M.Bases)
    {r : ℝ} (hr : 0 ≤ r) (h : H) (w : W) (hw : w ∈ E)
    (hh : eW (heightProjection T.character (h : L)) = r • w) (i : Fin M.letterCount) :
    ‖(M.boxBasis T hunimod eW E β r).equivFun
      (cartanIdealAdjointAutomorphism T H h (M.letter i))‖ ≤
    ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
      (cartanIdealResidualAutomorphism T H h (M.letter i))‖ := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.norm_wordBasis_lieMap_le line 94

Source documentation

A bound on generator images controls the map from any word basis to a basis with bounded structure constants.

theorem norm_wordBasis_lieMap_le
    (γ : M.Bases)
    (b : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (F : cartanRootIdeal H →ₗ⁅ℝ⁆ cartanRootIdeal H) {K A : ℝ} (hK : 0 ≤ K) (hA : 0 ≤ A)
    (hbracket : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ K)
    (hletter : ∀ i, ‖b.equivFun (F (M.letter i))‖ ≤ A) (v : cartanRootIdeal H) :
    ‖b.equivFun (F v)‖ ≤
      (finrank ℝ (cartanRootIdeal H) : ℝ) *
        (1 + (finrank ℝ (cartanRootIdeal H) : ℝ) ^ 2 * K) ^ M.wordDegreeBound *
        (1 + A) ^ M.wordDegreeBound *
          ‖(WordBasisSelections.basis M.letter M.wordList γ).equivFun v‖ := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_controlled_adjoint_bound line 141

Source documentation

Uniform polynomial coordinate control for Cartan actions with height inside a scaled template. The input basis is unscaled and need not maximize.

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

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