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) ^ p ≤ ∑ i in s, w i * z i ^ p
exact_mod_cast
  Real.rpow_arith_mean_le_arith_mean_rpow 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'