OAI/GroupTheory/PolycyclicRecognition/Analysis/TemplateBoxEnvelopes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_thickening_le line 23

   Source documentation

   Thickening the height template changes each weight by at most its operator norm times the thickening radius.

   theorem weightSupport_thickening_le {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
       {ε : ℝ} (hε : 0 ≤ ε) (i : I) :
       D.weightSupport (E + closedBall 0 ε) i ≤
         D.weightSupport E i + ‖(D.weight i).toContinuousLinearMap‖ * ε := by
   …

2. theorem OAI.PolycyclicRecognition.bracketWordExponent_le_add_of_le line 37
3. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_boxCost_thickening_constant line 53

   Source documentation

   The finite word list has one constant for all compact templates.

   theorem exists_boxCost_thickening_constant :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
         ∀ {ε : ℝ}, 0 ≤ ε → ∀ w : M.wordList,
           M.boxCost T hunimod eW (E + closedBall 0 ε) w ≤
             M.boxCost T hunimod eW E w + C * ε := by
   …

4. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_template_box_envelope_sequence line 84

   Source documentation

   Every enlarged-template box is contained in one fixed-template box with a common subexponential radius. The enlarged maximizing basis may change at every scale, or between endpoints at the same scale.

   theorem exists_template_box_envelope_sequence {N : Type*}
       (Exp : cartanRootIdeal H → N)
       (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)
       (scale ε R : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (hscale0 : ∀ n, 0 ≤ scale n) (hε0 : ∀ n, 0 ≤ ε n) (hε : Tendsto ε atTop (𝓝 0))
       (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R) :
       ∃ V : ℕ → ℝ, (∀ n, 0 ≤ V n) ∧ HasSubexponentialUpperBoundSeq scale V ∧
         ∀ n (γ : M.Bases),
   …

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