Theorems · Theorem · real analysis

NNReal.inner_le_Lp_mul_Lq

∀ {ι : Type u} (s : Finset ι) (f g : ι → NNReal) {p q : ℝ},
  p.HolderConjugate q → ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, 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. Version for sums over finite sets, with ℝ≥0-valued functions.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

5 results in Mathlib

Foundations

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