English
If f, g are nonnegative almost everywhere and belong to Lp and Lq, respectively, with p conjugate to q, then ∫ f g ≤ (∫ f^p)^{1/p} (∫ g^q)^{1/q}.
Русский
Если f, g неотрицательны почти всюду и принадлежат к Lp и Lq соответственно, где p сопряжено с q, то выполняется неравенство интеграла.
LaTeX
$$$\\displaystyle \\int_{\\alpha} f(a) g(a)\, d\\mu \\le \\left( \\int_{\\alpha} f(a)^p \\, d\\mu \\right)^{1/p} \\left( \\int_{\\alpha} g(a)^q \\, d\\mu \\right)^{1/q}$$$
Lean4
/-- Hölder's inequality for functions `α → ℝ`. The integral of the product of two nonnegative
functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
exponents. -/
theorem integral_mul_le_Lp_mul_Lq_of_nonneg {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f)
(hg_nonneg : 0 ≤ᵐ[μ] g) (hf : MemLp f (ENNReal.ofReal p) μ) (hg : MemLp g (ENNReal.ofReal q) μ) :
∫ a, f a * g a ∂μ ≤ (∫ a, f a ^ p ∂μ) ^ (1 / p) * (∫ a, g a ^ q ∂μ) ^ (1 / q) :=
by
have h_left : ∫ a, f a * g a ∂μ = ∫ a, ‖f a‖ * ‖g a‖ ∂μ :=
by
refine integral_congr_ae ?_
filter_upwards [hf_nonneg, hg_nonneg] with x hxf hxg
rw [Real.norm_of_nonneg hxf, Real.norm_of_nonneg hxg]
have h_right_f : ∫ a, f a ^ p ∂μ = ∫ a, ‖f a‖ ^ p ∂μ :=
by
refine integral_congr_ae ?_
filter_upwards [hf_nonneg] with x hxf
rw [Real.norm_of_nonneg hxf]
have h_right_g : ∫ a, g a ^ q ∂μ = ∫ a, ‖g a‖ ^ q ∂μ :=
by
refine integral_congr_ae ?_
filter_upwards [hg_nonneg] with x hxg
rw [Real.norm_of_nonneg hxg]
rw [h_left, h_right_f, h_right_g]
exact integral_mul_norm_le_Lp_mul_Lq hpq hf hg
