The Cauchy–Schwarz inequality for interval integrals #
For a function g on [a, b] whose square is integrable,
∫ₐᵇ g ≤ √(b - a) √(∫ₐᵇ g²) (TauCeti.integral_le_sqrt_mul_sqrt_integral_sq). This is the
estimate that turns an L² bound on a derivative into a uniform Hölder modulus of continuity
|f(t₂) - f(t₁)| ≤ √(t₂ - t₁) ‖f'‖_{L²}, as in the Sobolev embedding W^{1,2} ⊆ C^{1/2} in one
dimension.
It is the case f = 1, p = q = 2 of Hölder's inequality
MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg, restated for interval integrals with square
roots in place of the powers 1 / 2.
theorem
TauCeti.integral_le_sqrt_mul_sqrt_integral_sq
{g : ℝ → ℝ}
{a b : ℝ}
(hab : a ≤ b)
(hg2 : IntervalIntegrable (fun (t : ℝ) => g t ^ 2) MeasureTheory.volume a b)
:
The Cauchy–Schwarz inequality on an interval. For a function g on [a, b] with g²
integrable, ∫ₐᵇ g ≤ √(b - a) √(∫ₐᵇ g²).