Theorems · Theorem · real analysis

NNReal.Lp_add_le

∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p : ℝ},
  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)

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.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

3 results in Mathlib

Foundations

Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound