OAI/GroupTheory/PolycyclicRecognition/Analysis/ControlledPathErrorEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_controlled_path_error_envelope line 17

   Source documentation

   Linear path speed and logarithmic additive error have the precise subexponential bounds required by the path-lifting construction. The profile and short-switch errors fit one explicitly vanishing tolerance.

   theorem exists_controlled_path_error_envelope
       (scale η : ℕ → ℝ) (hs : Tendsto scale atTop atTop) (hs1 : ∀ n, 1 ≤ scale n)
       (hη0 : ∀ n, 0 ≤ η n) (hη : Tendsto η atTop (𝓝 0))
       (A B K : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hK : 0 ≤ K) :
       ∃ ε : ℕ → ℝ, (∀ n, 0 ≤ ε n) ∧ Tendsto ε atTop (𝓝 0) ∧
         HasSubexponentialUpperBoundSeq scale (fun n => A * scale n) ∧
         HasSubexponentialUpperBoundSeq scale (fun n => B * (1 + Real.log (2 + scale n))) ∧
         ∀ n, K * (B * (1 + Real.log (2 + scale n)) + 2) +
           (2 * scale n * η n + A * (1 + Real.log (2 + scale n))) ≤ scale n * ε n := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq