English
An equivalent formulation of the equality condition for the weighted AM-GM using a general Iff with a sum and weights.
Русский
Эквивалентное формулирование условия равенства в взвешенном AM-GM через эквивалентность
LaTeX
$$$\\text{Equality condition: }(\\prod z_i^{w_i}) = (\\sum w_i z_i)$ iff ...$$
Lean4
/-- **AM-GM inequality - equality condition**: This theorem provides the equality condition for the
weighted version of the AM-GM inequality for real-valued nonnegative functions. -/
theorem geom_mean_eq_arith_mean_weighted_iff (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 ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i :=
by
have h (i) (_ : i ∈ s) : w i * z i ≠ 0 → w i ≠ 0 := by apply left_ne_zero_of_mul
have h' (i) (_ : i ∈ s) : z i ^ w i ≠ 1 → w i ≠ 0 := by
by_contra!
obtain ⟨h1, h2⟩ := this
simp only [h2, rpow_zero, ne_self_iff_false] at h1
rw [← sum_filter_of_ne h, ← prod_filter_of_ne h', geom_mean_eq_arith_mean_weighted_iff']
· simp
· simp +contextual [(hw _ _).lt_iff_ne']
· rwa [sum_filter_ne_zero]
· simp_all only [ne_eq, mul_eq_zero, not_or, not_false_eq_true, implies_true, mem_filter]
