Theorems · Theorem · real analysis

NNReal.Lr_rpow_le_Lp_mul_Lq

∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q r : ℝ},
  p.HolderTriple q r → ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)

Hölder inequality: The (r-power of the) L^r norm of the product of two functions is bounded by the product of (the r-powers of) their L^p and L^q norms when p, q, and r form a Real.HolderTriple.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

3 results in Mathlib

Foundations

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