English
A Minkowski-type inequality for ENNReal: the Lp-norm of a sum is bounded by the sum of the Lp-norms.
Русский
Тип неравенства Минковского для ENNReal: норма по Lp сумм равна сумме норм по Lp.
LaTeX
$$$\\forall p≥1:\\; (\\int (f+g)^p)^{1/p} ≤ (\\int f^p)^{1/p} + (\\int g^p)^{1/p}$$$
Lean4
/-- **Minkowski's inequality for functions** `α → ℝ≥0∞`: the `ℒp` seminorm of the sum of two
functions is bounded by the sum of their `ℒp` seminorms. -/
theorem lintegral_Lp_add_le {p : ℝ} {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hp1 : 1 ≤ p) :
(∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p) :=
by
have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1
by_cases hf_top : ∫⁻ a, f a ^ p ∂μ = ⊤
· simp [hf_top, hp_pos]
by_cases hg_top : ∫⁻ a, g a ^ p ∂μ = ⊤
· simp [hg_top, hp_pos]
by_cases h1 : p = 1
· refine le_of_eq ?_
simp_rw [h1, one_div_one, ENNReal.rpow_one]
exact lintegral_add_left' hf _
have hp1_lt : 1 < p := by
refine lt_of_le_of_ne hp1 ?_
symm
exact h1
have hpq := Real.HolderConjugate.conjExponent hp1_lt
by_cases h0 : (∫⁻ a, (f + g) a ^ p ∂μ) = 0
· rw [h0, @ENNReal.zero_rpow_of_pos (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
exact zero_le _
have htop : (∫⁻ a, (f + g) a ^ p ∂μ) ≠ ⊤ := by
rw [← Ne] at hf_top hg_top
rw [← lt_top_iff_ne_top] at hf_top hg_top ⊢
exact lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1
exact lintegral_Lp_add_le_aux hpq hf hf_top hg hg_top h0 htop
