English
For Real-valued finite sequences f,g, the Lp-norm of the sum is bounded by the sum of Lp-norms.
Русский
Для вещественных последовательностей f,g ограничение нормы Lp суммы на сумму норм Lp каждого слагаемого.
LaTeX
$$$\left(\sum_{i\in s} |f_i+g_i|^p\right)^{1/p} \le \left(\sum_{i\in s} |f_i|^p\right)^{1/p} + \left(\sum_{i\in s} |g_i|^p\right)^{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 `Real`-valued functions. -/
theorem Lp_add_le (hp : 1 ≤ p) :
(∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p) :=
by
have := NNReal.coe_le_coe.2 (NNReal.Lp_add_le s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩) hp)
push_cast at this
refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this <;>
simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le, rpow_le_rpow]
