PPTErrorEnvelope.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An actual vanishing envelope for an iterated eventual error bound.

theorem OAI.TotientAsymptotic.ppt_iterated_error_envelope line 14

Source documentation

Turn an iterated small-error estimate into one envelope valid at every fixed index. The infimum is taken over eventual normalized upper bounds; its approximation needs no attainment or uniform threshold in the index.

theorem ppt_iterated_error_envelope (E : ℕ→ℝ→ℝ) (S : ℝ→ℝ)
    (hS : ∀ᶠ x : ℝ in atTop, 0 < S x)
    (hbound : ∃ C : ℝ, ∀ᶠ x : ℝ in atTop, ∀ P : ℕ, E P x ≤ C*S x)
    (hsmall : ∀ ε : ℝ, 0 < ε → ∀ᶠ P : ℕ in atTop,
      ∀ᶠ x : ℝ in atTop, E P x ≤ ε*S x) :
    ∃ δ : ℕ→ℝ, Tendsto δ atTop (𝓝 0) ∧
      ∀ P : ℕ, ∀ ε : ℝ, 0 < ε →
        ∀ᶠ x : ℝ in atTop, E P x ≤ (δ P+ε)*S x := by
…

Mentions: OAI.TotientAsymptotic.P