English
Equality condition for the weighted AM-GM when the weights are nonnegative and sum to 1: z_j equals the weighted sum of the z_i's for all j in the index set.
Русский
Условие равенства в взвешенном AM-GM: если веса ненегативны и сумма равна 1, тогда z_j равно взвешенной сумме z_i для каждого j.
LaTeX
$$$\\forall j\\in s,\\; z_j = \\sum_{i\\in s} w_i z_i$$$
Lean4
theorem geom_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1)
(hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : ∏ i ∈ s, z i ^ w i = x :=
calc
∏ i ∈ s, z i ^ w i = ∏ i ∈ s, x ^ w i :=
by
refine prod_congr rfl fun i hi => ?_
rcases eq_or_ne (w i) 0 with h₀ | h₀
· rw [h₀, rpow_zero, rpow_zero]
· rw [hx i hi h₀]
_ = x := by
rw [← rpow_sum_of_nonneg _ hw, hw', rpow_one]
have : (∑ i ∈ s, w i) ≠ 0 := by
rw [hw']
exact one_ne_zero
obtain ⟨i, his, hi⟩ := exists_ne_zero_of_sum_ne_zero this
rw [← hx i his hi]
exact hz i his
