English
For ENNReal-valued finite sums, Minkowski holds: (∑ (f_i+g_i)^p)^{1/p} ≤ (∑ f_i^p)^{1/p} + (∑ g_i^p)^{1/p}.
Русский
Для ENNReal естественных значений неравенство Минковского: аналогично.
LaTeX
$$$\bigl(\sum_{i\in s} (f_i+g_i)^p\bigr)^{1/p} \le \bigl(\sum_{i\in s} f_i^p\bigr)^{1/p} + \bigl(\sum_{i\in s} g_i^p\bigr)^{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 `ℝ`-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_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) {A B : ℝ} (hA : 0 ≤ A)
(hB : 0 ≤ B) (hfA : HasSum (fun i => f i ^ p) (A ^ p)) (hgB : HasSum (fun i => g i ^ p) (B ^ p)) :
∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p) :=
by
lift f to ι → ℝ≥0 using hf
lift g to ι → ℝ≥0 using hg
lift A to ℝ≥0 using hA
lift B to ℝ≥0 using hB
beta_reduce at hfA hgB
norm_cast at hfA hgB
obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB
use C
beta_reduce
norm_cast
exact ⟨zero_le _, hC₁, hC₂⟩
