PolynomialPrefixEnvelope.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial losses preserve the common vanishing prefix envelope

theorem OAI.PolycyclicRecognition.exists_polynomial_exponential_envelope line 14

Source documentation

The fixed polynomial loss in nilpotent multiplication only changes the vanishing error exponent. The bound holds at every scale, not just eventually.

theorem exists_polynomial_exponential_envelope
    (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
    (hscale1 : ∀ n, 1 ≤ scale n)
    (ε : ℕ → ℝ) (hε0 : ∀ n, 0 ≤ ε n) (hε : Tendsto ε atTop (𝓝 0))
    (D : ℝ) (hD : 0 ≤ D) (d : ℕ) :
    ∃ η : ℕ → ℝ, (∀ n, 0 ≤ η n) ∧ Tendsto η atTop (𝓝 0) ∧
      ∀ n, D * (1 + Real.exp (scale n * ε n)) ^ d ≤ Real.exp (scale n * η n) := by
…