Abstract real inequalities for the stream-difference estimate

A Cauchy–Schwarz inequality for integrals from a pointwise nonnegative quadratic form, and the final real-number step turning the energy balance into the η/κ bound.

theorem AVenhance.Infra.Section5.RelativeError.sq_integral_le_of_quadratic_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q r : α → ℝ} (hp : MeasureTheory.Integrable p μ) (hq : MeasureTheory.Integrable q μ) (hr : MeasureTheory.Integrable r μ) (h : ∀ᵐ (x : α) ∂μ, ∀ (l : ℝ), 0 ≤ l ^ 2 * p x + 2 * l * q x + r x) : (∫ (x : α), q x ∂μ) ^ 2 ≤ (∫ (x : α), p x ∂μ) * ∫ (x : α), r x ∂μ

Cauchy–Schwarz from a pointwise nonnegative quadratic form.

theorem AVenhance.Infra.Section5.RelativeError.stream_final_real {κ η A B C E l : ℝ} (hκ : 0 < κ) (hη : 0 ≤ η) (hA : 0 ≤ A) (hl : 0 ≤ l) (hid : l + 2 * κ * A = -2 * C) (hCE : C ^ 2 ≤ E * A) (hE : E ≤ η ^ 2 * B) : √κ * √A ≤ η / κ * (√κ * √B)

The final real step: from the energy balance l + 2κA = -2C, the Cauchy–Schwarz bound C² ≤ E A and E ≤ η² B, conclude √κ √A ≤ (η/κ) (√κ √B).