English
If the z_i are constant equal to x on the support where w_i ≠ 0, then the geometric mean equals x.
Русский
Если все z_i равны константе x на поддержке весов, тогда геометрическая средняя равна x.
LaTeX
$$$\\prod_{i\\in s} z_i^{w_i} = x$ if all $z_i = x$ whenever $w_i \\neq 0$$$
Lean4
/-- **AM-GM inequality**: The **geometric mean is less than or equal to the arithmetic mean. -/
theorem geom_mean_le_arith_mean {ι : Type*} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
(hw' : 0 < ∑ i ∈ s, w i) (hz : ∀ i ∈ s, 0 ≤ z i) :
(∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ ≤ (∑ i ∈ s, w i * z i) / (∑ i ∈ s, w i) :=
by
convert geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz using 2
· rw [← finset_prod_rpow _ _ (fun i hi => rpow_nonneg (hz _ hi) _) _]
refine Finset.prod_congr rfl (fun _ ih => ?_)
rw [div_eq_mul_inv, rpow_mul (hz _ ih)]
· simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]
· exact fun _ hi => div_nonneg (hw _ hi) (le_of_lt hw')
· simp_rw [div_eq_mul_inv, ← Finset.sum_mul]
exact mul_inv_cancel₀ (by linarith)
