CartanConjugationHeightBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The exact exponential height loss in conjugated Cartan boxes

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_adjoint_groupBox_height_bound line 34

Source documentation

Conjugation changes a scaled box by a polynomial in the Cartan logarithm and an exponential in its height. The height coefficient is independent of the template, its scale and its maximizing basis.

theorem exists_adjoint_groupBox_height_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ (A K : ℝ) (p : ℕ), 0 ≤ A ∧ 0 ≤ K ∧
      ∀ {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) (R : ℝ) (g : N),
      g ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r R →
      M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h g ∈
        M.groupBox T hunimod eW (Exp ∘ eN) E β r
          (A * (1 + ‖(finBasis ℝ H).equivFun h‖) ^ p *
            Real.exp (K * ‖eW (heightProjection T.character (h : L))‖) * R) := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_adjoint_groupBox_scale_margin line 87

Source documentation

A strict gain in box scale absorbs the conjugation height loss. The remaining radius shows the precise exponent margin used in the basepoint sampling comparison.

theorem exists_adjoint_groupBox_scale_margin
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ (A K : ℝ) (p : ℕ), 0 ≤ A ∧ 0 ≤ K ∧
      ∀ {E : Set W}, IsCompact E → E.Nonempty → ∀ β : M.Bases,
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ lo : ℝ, (∀ w : M.wordList, lo ≤ M.boxCost T hunimod eW E w) →
      ∀ s t : ℝ, 0 < s → s ≤ t → ∀ (h : H) (R : ℝ) (g : N),
      g ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β s R →
      M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin h g ∈
        M.groupBox T hunimod eW (Exp ∘ eN) E β t
          (A * (1 + ‖(finBasis ℝ H).equivFun h‖) ^ p * R *
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_eventual_adjoint_box_inclusion line 126

Source documentation

A positive exponent margin absorbs every polynomial logarithmic loss and every subexponential input radius. This turns the quantitative bound into the exact box inclusion required by Haar-density domination.

theorem exists_eventual_adjoint_box_inclusion
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) β.val)
    (lo : ℝ) (hlo : ∀ w : M.wordList, lo ≤ M.boxCost T hunimod eW E w) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ scale source target RH R heightBound : ℕ → ℝ,
      Tendsto scale atTop atTop →
      (∀ n, 0 ≤ RH n) → (∀ n, 0 ≤ R n) →
      HasSubexponentialUpperBoundSeq scale RH → HasSubexponentialUpperBoundSeq scale R →
      ∀ ε : ℝ, 0 < ε →
      (∀ᶠ n in atTop, 0 < source n ∧ source n ≤ target n ∧
…

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