English
The Lp-norm of a sum is bounded by the sum of the Lp-norms: (∑ (f_i+g_i)^p)^{1/p} ≤ (∑ f_i^p)^{1/p} + (∑ g_i^p)^{1/p}.
Русский
Норма 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 `NNReal`-valued functions. -/
theorem Lp_add_le (f g : ι → ℝ≥0) {p : ℝ} (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
-- The result is trivial when `p = 1`, so we can assume `1 < p`.
rcases eq_or_lt_of_le hp with (rfl | hp)
· simp [Finset.sum_add_distrib]
have hpq := Real.HolderConjugate.conjExponent hp
have := isGreatest_Lp s (f + g) hpq
simp only [Pi.add_apply, add_mul, sum_add_distrib] at this
rcases this.1 with ⟨φ, hφ, H⟩
rw [← H]
exact add_le_add ((isGreatest_Lp s f hpq).2 ⟨φ, hφ, rfl⟩) ((isGreatest_Lp s g hpq).2 ⟨φ, hφ, rfl⟩)
