Theorems · Theorem · real analysis

NNReal.summable_and_inner_le_Lp_mul_Lq_tsum

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

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. A version for NNReal-valued functions. For an alternative version, convenient if the infinite sums are already expressed as p-th powers, see inner_le_Lp_mul_Lq_hasSum.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

3 results in Mathlib

Foundations

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