English
Hölder's inequality for functions α → ℝ≥0∞: ∫ f g ≤ (∫ f^p)^{1/p} (∫ g^q)^{1/q} for p,q conjugate and a.e. measurable f,g.
Русский
Неравенство Хольдера для функций α → ℝ≥0∞: ∫ f g ≤ (∫ f^p)^{1/p} (∫ g^q)^{1/q}, где p,q сопряжены.
LaTeX
$$$\\forall α,[MeasurableSpace α], μ:Measure α, p,q\\in\\mathbb{R},\\; hpq: p.HolderConjugate q,\\; f,g: α\\to\\mathbb{R}_{\\ge 0}^{∞},\\; AEMeasurable f μ, AEMeasurable g μ \\,\\Rightarrow \\\\ \\int f g \\le (\\int f^p)^{1/p} (\\int g^q)^{1/q}$$$
Lean4
/-- Hölder's inequality for functions `α → ℝ≥0∞`. The integral of the product of two functions
is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
exponents. -/
theorem lintegral_mul_le_Lp_mul_Lq (μ : Measure α) {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ≥0∞}
(hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
(∫⁻ a, (f * g) a ∂μ) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ q ∂μ) ^ (1 / q) :=
by
by_cases hf_zero : ∫⁻ a, f a ^ p ∂μ = 0
· refine Eq.trans_le ?_ (zero_le _)
exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.nonneg hf hf_zero
by_cases hg_zero : ∫⁻ a, g a ^ q ∂μ = 0
· refine Eq.trans_le ?_ (zero_le _)
rw [mul_comm]
exact lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero hpq.symm.nonneg hg hg_zero
by_cases hf_top : ∫⁻ a, f a ^ p ∂μ = ⊤
· exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.pos hpq.symm.nonneg hf_top hg_zero
by_cases hg_top : ∫⁻ a, g a ^ q ∂μ = ⊤
· rw [mul_comm, mul_comm ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p))]
exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.symm.pos hpq.nonneg hg_top hf_zero
exact ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero
