OAI/GroupTheory/PolycyclicRecognition/Algebra/BoundedPrefixEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_vanishing_exponential_envelope line 16

   Source documentation

   A constant coordinate radius can be written as an exponential envelope whose normalized exponent tends to zero along the scale sequence.

   theorem exists_vanishing_exponential_envelope
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (hscale1 : ∀ n, 1 ≤ scale n) (D : ℝ) :
       ∃ ε : ℕ → ℝ, (∀ n, 0 ≤ ε n) ∧ Tendsto ε atTop (𝓝 0) ∧
         ∀ n, D ≤ Real.exp (scale n * ε n) := by
   …

2. theorem OAI.PolycyclicRecognition.enlarged_prefix_vanishing_envelope line 36

   Source documentation

   Enlarging nonnegative word weights preserves the common prefix bound, so all prefix coordinates satisfy the vanishing exponential error required by neighboring-sheet affinity. The basis and weights may vary with scale.

   theorem enlarged_prefix_vanishing_envelope
       {L J K : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J]
       (b : ℕ → Basis J ℝ L) (cost : ℕ → J → ℝ)
       (hcost : ∀ n j, 0 ≤ cost n j)
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (hscale1 : ∀ n, 1 ≤ scale n)
       (vertex : ℕ → K → L) (D : ℝ)
       (hbound : ∀ n k,
         ‖(exponentialRescaleBasis (b n) (cost n) (scale n)).equivFun (vertex n k)‖ ≤ D)
       {δ : ℝ} (hδ : 0 ≤ δ) :
       ∃ ε : ℕ → ℝ, (∀ n, 0 ≤ ε n) ∧ Tendsto ε atTop (𝓝 0) ∧
         ∀ n k,
   …

   Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis