Extended-Real Scaled Quadratic Bound

This vendored algebraic lemma gives a scaled quadratic upper bound in the extended nonnegative reals.

Let $\varepsilon,a\in[0,\infty]$ with $\varepsilon\neq0$ and $\varepsilon\neq\infty$. Then

The inequality is a technical estimate useful for controlling a quantity by a scale parameter and a quadratic error term.

Formalization Note. All quantities are ENNReal; $\varepsilon^{-1}$ is the ENNReal inverse, and the hypotheses exclude both zero and top.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem le_add_inv_mul_sq {ε : ℝ≥0∞} (h0 : ε ≠ 0) (htop : ε ≠ ⊤) (a : ℝ≥0∞) :
    a ≤ ε + ε⁻¹ * a ^ 2

Module navigation

Module: LevyStochCalc/Ito/VectorItoVersionLimit.

Next: clampMesh_mono_window.

Source excerpt, lines 47–48 · Frozen source 408915f.