Theorems · Theorem · real analysis

ENNReal.inner_le_Lp_mul_Lq

∀ {ι : Type u} (s : Finset ι) (f g : ι → ENNReal) {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

1 results in Mathlib

Foundations

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