CartanNeighborSuffixRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One logarithmic coordinate rate for both neighboring suffixes

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_neighbor_suffix_coordinate_rate line 29

Source documentation

The actual box product estimate supplies logarithms of the suffix and its product with the neighboring step, with a single vanishing coordinate rate. No separate product-suffix error estimate is assumed.

theorem exists_neighbor_suffix_coordinate_rate
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) β.val)
    (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop) (hspos : ∀ n, 0 < scale n)
    (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R)
    (k₀ k : ℕ → F.N.carrier)
    (hk₀ : ∀ n, k₀ n ∈ M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv) E β (scale n) (R n))
    (hk : ∀ n, k n ∈ M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv) E β (scale n) (R n)) :
    ∃ (v₀ v₁ : ℕ → cartanRootIdeal H) (ε : ℕ → ℝ),
…

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