Theorems · Theorem · real analysis

NNReal.Lp_add_le_hasSum

∀ {ι : Type u} {f g : ι → NNReal} {A B : NNReal} {p : ℝ},
  1 ≤ p →
    HasSum (fun i => f i ^ p) (A ^ p) →
      HasSum (fun i => g i ^ p) (B ^ p) → ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ 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 not already expressed as p-th powers, see Lp_add_le_tsum_of_nonneg.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

1 results in Mathlib

Foundations

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