English
A compounded Hölder inequality for sums of powers: the integral of a sum of functions raised to p is controlled by the pth roots of their separate integrals.
Русский
Сложенное неравенство Хольдера для сумм функций: интеграл суммы в степени p ограничен корнем p-й степени от суммарных интегралов.
LaTeX
$$$\\int (f+g)^p dμ ≤ (\\int f^p dμ) + (\\int g^p dμ)$ для p≥1, и соответствующая модификация для p≤1$$
Lean4
theorem lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ≥0∞}
(hf : AEMeasurable f μ) (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) (hg : AEMeasurable g μ)
(hg_top : (∫⁻ a, g a ^ p ∂μ) ≠ ⊤) :
(∫⁻ a, (f + g) a ^ p ∂μ) ≤
((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ a, (f a + g a) ^ p ∂μ) ^ (1 / q) :=
by
calc
(∫⁻ a, (f + g) a ^ p ∂μ) ≤ ∫⁻ a, (f + g) a * (f + g) a ^ (p - 1) ∂μ :=
by
gcongr with a
by_cases h_zero : (f + g) a = 0
· rw [h_zero, ENNReal.zero_rpow_of_pos hpq.pos]
exact zero_le _
by_cases h_top : (f + g) a = ⊤
· rw [h_top, ENNReal.top_rpow_of_pos hpq.sub_one_pos, ENNReal.top_mul_top]
exact le_top
refine le_of_eq ?_
nth_rw 2 [← ENNReal.rpow_one ((f + g) a)]
rw [← ENNReal.rpow_add _ _ h_zero h_top, add_sub_cancel]
_ = (∫⁻ a : α, f a * (f + g) a ^ (p - 1) ∂μ) + ∫⁻ a : α, g a * (f + g) a ^ (p - 1) ∂μ :=
by
have h_add_m : AEMeasurable (fun a : α => (f + g) a ^ (p - 1 : ℝ)) μ := (hf.add hg).pow_const _
have h_add_apply :
(∫⁻ a : α, (f + g) a * (f + g) a ^ (p - 1) ∂μ) = ∫⁻ a : α, (f a + g a) * (f + g) a ^ (p - 1) ∂μ := rfl
simp_rw [h_add_apply, add_mul]
rw [lintegral_add_left' (hf.mul h_add_m)]
_ ≤ ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ a, (f a + g a) ^ p ∂μ) ^ (1 / q) :=
by
rw [add_mul]
gcongr
· exact lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow hpq hf (hf.add hg) hf_top
· exact lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow hpq hg (hf.add hg) hg_top
