English
Let s be a finite index set, weights w_i ≥ 0 with total sum 1, and nonnegative values z_i. Then the weighted geometric mean is at most the weighted arithmetic mean: (∏ z_i^{w_i}) ≤ ∑ w_i z_i.
Русский
Пусть S конечен; веса w_i ≥ 0 суммируются до 1; z_i ≥ 0. Тогда взвешенная геометрическая средняя не превосходит взвешенную арифметическую: \\prod z_i^{w_i} ≤ ∑ w_i z_i.
LaTeX
$$$\\prod_{i\\in s} z_i^{w_i} \\le \\sum_{i\\in s} w_i z_i$$$
Lean4
/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean, weighted
version for real-valued nonnegative functions. -/
theorem geom_mean_le_arith_mean_weighted (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1)
(hz : ∀ i ∈ s, 0 ≤ z i) : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i := by
-- If some number `z i` equals zero and has non-zero weight, then LHS is 0 and RHS is nonnegative.
by_cases A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
· rcases A with ⟨i, his, hzi, hwi⟩
rw [prod_eq_zero his]
· exact sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)
· rw [hzi]
exact zero_rpow hwi
· simp only [not_exists, not_and, Ne, Classical.not_not] at A
have := convexOn_exp.map_sum_le hw hw' fun i _ => Set.mem_univ <| log (z i)
simp only [exp_sum, smul_eq_mul, mul_comm (w _) (log _)] at this
convert this using 1 <;> [apply prod_congr rfl; apply sum_congr rfl] <;> intro i hi
· rcases eq_or_lt_of_le (hz i hi) with hz | hz
· simp [A i hi hz.symm]
· exact rpow_def_of_pos hz _
· rcases eq_or_lt_of_le (hz i hi) with hz | hz
· simp [A i hi hz.symm]
· rw [exp_log hz]
