no goals
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
exact_mod_cast
  Real.arith_mean_le_rpow_mean s _ _ (fun i _ => (w i).coe_nonneg) (by exact_mod_cast hw')
    (fun i _ => (z i).coe_nonneg) hp
no goals
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, ↑(w i) = 1
exact_mod_cast hw'