OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoupledRecurrenceCells.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coupled_interval_recurrence_cells line 33

   Source documentation

   The initial cell translation and the inside-sheet conjugation are both controlled in the containing template. The denominator is an exact radius power, and is subexponential. No independence after restriction is used.

   theorem exists_coupled_interval_recurrence_cells
       (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)
       (s : Fin M.letterCount → ℝ)
       (hs : ∀ i, s i ≤ (M.supportIn T hunimod eW).weightSupport E i)
       {m : ℕ} (letters : Fin m → Fin M.letterCount)
       (scale R : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (hscale0 : ∀ n, 0 ≤ scale n) (hR0 : ∀ n, 0 ≤ R n)
       (hR : HasSubexponentialUpperBoundSeq scale R)
       (ρ : ℝ) (hρ : 0 ≤ ρ) (k₀ : ℕ → N) (k : ℕ → ℕ → N)
   …

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