English
If HasSum of f^p and g^p exist, there exists C with HasSum of (f+g)^p bounded by C^p when adding.
Русский
Если существуют суммы HasSum для f^p и g^p, то существует C с HasSum для (f+g)^p и неравенство по C^p.
LaTeX
$$$\exists C$ such that $C \le A+B$ и HasSum (f_i+g_i)^p = C^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 not already expressed as `p`-th powers, see `Lp_add_le_tsum_of_nonneg`. -/
theorem Lp_add_le_hasSum {f g : ι → ℝ≥0} {A B : ℝ≥0} {p : ℝ} (hp : 1 ≤ p) (hf : HasSum (fun i => f i ^ p) (A ^ p))
(hg : HasSum (fun i => g i ^ p) (B ^ p)) : ∃ C, C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p) :=
by
have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne'
obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hp']
have hB : B = (∑' i : ι, g i ^ p) ^ (1 / p) := by rw [hg.tsum_eq, rpow_inv_rpow_self hp']
refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), ?_, ?_⟩
· simpa [hA, hB] using H₂
· simpa only [rpow_self_rpow_inv hp'] using H₁.hasSum
