Theorems · Theorem · real analysis

NNReal.inner_le_weight_mul_Lp

∀ {ι : Type u} (s : Finset ι) {p : ℝ},
  1 ≤ p → ∀ (w f : ι → NNReal), ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Weighted Hölder inequality.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

2 results in Mathlib

Foundations

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