CartanSmallHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugating a small error by a Cartan factor of small height

The full logarithm of the Cartan factor may be polynomially large. Only its height contributes to the exponential factor; the residual action contributes a fixed polynomial. This distinction is needed for thickened probe endpoints.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_small_height_adjoint_bound line 30

Source documentation

The estimate is uniform over all input word bases. The output uses one fixed zero-template basis.

theorem exists_small_height_adjoint_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW {0}) β.val) :
    ∃ (A K : ℝ) (p : ℕ), 0 ≤ A ∧ 0 ≤ K ∧
      ∀ (γ : M.Bases) (h : H) (v : cartanRootIdeal H),
        ‖(M.boxBasis T hunimod eW {0} β 1).equivFun
          (cartanIdealAdjointAutomorphism T H h v)‖ ≤
        A * (1 + ‖(finBasis ℝ H).equivFun h‖) ^ p *
          Real.exp (K * ‖eW (heightProjection T.character (h : L))‖) *
            ‖(WordBasisSelections.basis M.letter M.wordList γ).equivFun v‖ := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_small_height_adjoint_bound_in_basis line 76

Source documentation

The output can use the fixed adapted ideal-section basis. Its coordinate change only changes the constant, not the height exponent.

theorem exists_small_height_adjoint_bound_in_basis
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {J : Type*} [Fintype J] (b : Basis J ℝ (cartanRootIdeal H)) :
    ∃ (A K : ℝ) (p : ℕ), 0 ≤ A ∧ 0 ≤ K ∧
      ∀ (γ : M.Bases) (h : H) (v : cartanRootIdeal H),
        ‖b.equivFun (cartanIdealAdjointAutomorphism T H h v)‖ ≤
        A * (1 + ‖(finBasis ℝ H).equivFun h‖) ^ p *
          Real.exp (K * ‖eW (heightProjection T.character (h : L))‖) *
            ‖(WordBasisSelections.basis M.letter M.wordList γ).equivFun v‖ := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_small_height_adjoint_sequence_bound line 108

Source documentation

Polynomial Cartan-log growth and small height preserve a small exponential error. The constant is independent of the chosen small δ and of every point in the family.

theorem exists_small_height_adjoint_sequence_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {J : Type*} [Fintype J] (b : Basis J ℝ (cartanRootIdeal H))
    (scale RH RE : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hRH0 : ∀ n, 0 ≤ RH n)
    (hRH : HasSubexponentialUpperBoundSeq scale RH)
    (hRE : HasSubexponentialUpperBoundSeq scale RE) :
    ∃ B : ℝ, 0 < B ∧ ∀ δ : ℝ, 0 < δ → ∀ᶠ n in atTop,
      ∀ (γ : M.Bases) (h : H) (v : cartanRootIdeal H),
        ‖(finBasis ℝ H).equivFun h‖ ≤ RH n →
        ‖eW (heightProjection T.character (h : L))‖ ≤ δ * scale n →
        ‖(WordBasisSelections.basis M.letter M.wordList γ).equivFun v‖ ≤
…

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