English
A version of a Minkowski-type bound when p ≤ 1, multiplying by the sum of integrals under a power p.
Русский
Версия неравенства для p ≤ 1, оценивающая норму суммы через сумму норм на p-степени.
LaTeX
$$$0≤p≤1,\\; ∫ f^p, ∫ g^p < ∞ \\Rightarrow ∫ f^p + ∫ g^p ≥ ∫ (f+g)^p$$$
Lean4
/-- Variant of Minkowski's inequality for functions `α → ℝ≥0∞` in `ℒp` with `p ≤ 1`: the `ℒp`
seminorm of the sum of two functions is bounded by a constant multiple of the sum
of their `ℒp` seminorms. -/
theorem lintegral_Lp_add_le_of_le_one {p : ℝ} {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
(∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤
(2 : ℝ≥0∞) ^ (1 / p - 1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) :=
by
rcases eq_or_lt_of_le hp0 with (rfl | hp)
· simp only [Pi.add_apply, rpow_zero, lintegral_one, _root_.div_zero, zero_sub]
norm_num
rw [rpow_neg, rpow_one, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]
calc
(∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ ((∫⁻ a, f a ^ p ∂μ) + ∫⁻ a, g a ^ p ∂μ) ^ (1 / p) :=
by
rw [← lintegral_add_left' (hf.pow_const p)]
gcongr with a
exact rpow_add_le_add_rpow _ _ hp0 hp1
_ ≤ (2 : ℝ≥0∞) ^ (1 / p - 1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) :=
rpow_add_le_mul_rpow_add_rpow _ _ ((one_le_div hp).2 hp1)
