OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteProfileEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_finite_profile_envelope line 17

   Source documentation

   Eventual uniform control of a finite family can be extended to every scale without changing the vanishing error sequence on its tail. The size of the family is allowed to grow with the scale.

   theorem exists_finite_profile_envelope {J : ℕ → Type*} [∀ n, Fintype (J n)]
       (base : ℕ → ℝ≥0) (err : ∀ n, J n → ℝ≥0) (η : ℕ → ℝ)
       (hη : Tendsto η atTop (𝓝 0))
       (hb : ∀ᶠ n in atTop, (base n : ℝ) ≤ η n)
       (he : ∀ᶠ n in atTop, ∀ j, (err n j : ℝ) ≤ η n) :
       ∃ ε : ℕ → ℝ, Tendsto ε atTop (𝓝 0) ∧
         (∀ n, η n ≤ ε n) ∧ (∀ n, (base n : ℝ) ≤ ε n) ∧
         (∀ n j, (err n j : ℝ) ≤ ε n) := by
   …