English
Let p ≥ 1 and f_i,g_i ≥ 0 with Summable f_i^p and Summable g_i^p; then the sum of (f_i+g_i)^p is summable and (∑ (f_i+g_i)^p)^{1/p} ≤ (∑ f_i^p)^{1/p} + (∑ g_i^p)^{1/p}.
Русский
Пусть p ≥ 1 и f_i,g_i ≥ 0 с суммируемыми f_i^p и g_i^p; тогда ∑ (f_i+g_i)^p суммируем и (∑ (f_i+g_i)^p)^{1/p} ≤ (∑ f_i^p)^{1/p} + (∑ g_i^p)^{1/p}.
LaTeX
$$$(\sum_i (f_i+g_i)^p)^{1/p} \le (\sum_i f_i^p)^{1/p} + (\sum_i g_i^p)^{1/p}$ (with summability hypotheses)$$
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 `ℝ`-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_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i)
(hf_sum : Summable fun i => f i ^ p) (hg_sum : 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
lift f to ι → ℝ≥0 using hf
lift g to ι → ℝ≥0 using hg
beta_reduce at *
norm_cast0 at *
exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum
