English
The Lp-norm of the infinite sum is bounded by the sum of the Lp-norms, assuming the sums exist.
Русский
Пусть существует бесконечная сумма; тогда норма Lp суммы не превосходит сумму норм Lp слагаемых.
LaTeX
$$$\left(\sum_{i} (f_i+g_i)^p \right)^{1/p} \le \left(\sum_i f_i^p\right)^{1/p} + \left(\sum_i g_i^p\right)^{1/p}$$$
Lean4
/-- **Minkowski inequality**: the `L_p` seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
exist. A version for `NNReal`-valued functions. For an alternative version, convenient if the
infinite sums are already expressed as `p`-th powers, see `Lp_add_le_hasSum_of_nonneg`. -/
theorem Lp_add_le_tsum {f g : ι → ℝ≥0} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun i => f i ^ p)
(hg : Summable fun i => g i ^ p) :
(Summable fun i => (f i + g i) ^ p) ∧
(∑' i, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p) :=
by
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
have H₁ : ∀ s : Finset ι, (∑ i ∈ s, (f i + g i) ^ p) ≤ ((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p :=
by
intro s
rw [one_div, ← NNReal.rpow_inv_le_iff pos, ← one_div]
refine le_trans (Lp_add_le s f g hp) (add_le_add ?_ ?_) <;> rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr pos)] <;>
refine Summable.sum_le_tsum _ (fun _ _ => zero_le _) ?_
exacts [hf, hg]
have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p) :=
by
refine ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩
rintro a ⟨s, rfl⟩
exact H₁ s
have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
refine ⟨H₂, ?_⟩
rw [one_div, NNReal.rpow_inv_le_iff pos, ← one_div]
exact H₂.tsum_le_of_sum_le H₁
