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