Theorems · Theorem · real analysis

NNReal.Lp_add_le_tsum

∀ {ι : Type u} {f g : ι → NNReal} {p : ℝ},
  1 ≤ p →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ p) →
        (Summable fun i => (f i + g i) ^ p) ∧
          (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

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 NNReal-valued functions. For an alternative version, convenient if the infinite sums are already expressed as p-th powers, see Lp_add_le_hasSum_of_nonneg.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

4 results in Mathlib

Foundations

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