English
For p ≥ 1 and nonnegative f_i,g_i indexed by i in s, the p-norm of the sum is at most the sum of the p-norms: (∑ (f_i+g_i)^p)^{1/p} ≤ (∑ f_i^p)^{1/p} + (∑ g_i^p)^{1/p}.
Русский
Для p ≥ 1 и неположительных f_i,g_i на индексы i в s выполняется: (∑ (f_i+g_i)^p)^{1/p} ≤ (∑ f_i^p)^{1/p} + (∑ g_i^p)^{1/p}.
LaTeX
$$$\biggl(\sum_{i\in s} (f_i+g_i)^p\biggr)^{1/p} \le \biggl(\sum_{i\in s} f_i^p\biggr)^{1/p} + \biggl(\sum_{i\in s} g_i^p\biggr)^{1/p}$$$
Lean4
/-- **Minkowski inequality**: the `L_p` seminorm of the sum of two vectors is less than or equal
to the sum of the `L_p`-seminorms of the summands. A version for `ℝ`-valued nonnegative
functions. -/
theorem Lp_add_le_of_nonneg (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) :
(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p) := by
convert Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1] <;> apply sum_congr rfl <;> intro i hi <;>
simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]
