Theorems · Theorem · real analysis

Real.compact_inner_le_weight_mul_Lp_of_nonneg

∀ {ι : Type u} (s : Finset ι) {p : ℝ},
  1 ≤ p →
    ∀ {w f : ι → ℝ},
      (∀ (i : ι), 0 ≤ w i) →
        (∀ (i : ι), 0 ≤ f i) →
          (s.expect fun i => w i * f i) ≤ (s.expect fun i => w i) ^ (1 - p⁻¹) * (s.expect fun i => w i * f i ^ p) ^ p⁻¹

Weighted Hölder inequality in terms of Finset.expect.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

0 results in Mathlib

Foundations

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