Source indexedtheorem · leanprover/lean4:v4.32.0

ENNReal.sq_lintegral_mul_le_mul_lintegral_sq

Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:94 to 102

Source documentation

Cauchy–Schwarz inequality for functions α → ℝ≥0∞ (Hölder's inequality squared).

Exact Lean statement

theorem sq_lintegral_mul_le_mul_lintegral_sq {f g : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    (∫⁻ a, f a * g a ∂μ) ^ 2 ≤ (∫⁻ a, f a ^ 2 ∂μ) * ∫⁻ a, g a ^ 2 ∂μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem sq_lintegral_mul_le_mul_lintegral_sq {f g : α → ℝ≥0∞}    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :    (∫⁻ a, f a * g a ∂μ) ^ 2 ≤ (∫⁻ a, f a ^ 2 ∂μ) * ∫⁻ a, g a ^ 2 ∂μ := by  convert! pow_le_pow_left₀ zero_le    (lintegral_mul_le_Lp_mul_Lq μ Real.HolderConjugate.two_two hf hg) 2  rw [mul_pow, ← ENNReal.rpow_natCast, ← ENNReal.rpow_mul, ← ENNReal.rpow_natCast,    ← ENNReal.rpow_mul, show (1 : ℝ) / 2 * (2 : ℕ) = 1 by norm_num, ENNReal.rpow_one,    ENNReal.rpow_one]  simp_rw [show (2 : ℝ) = (2 : ℕ) by rfl, ← ENNReal.rpow_natCast]