English
If at least two z_i are different under positive weights, the AM-GM inequality is strict: the geometric mean is strictly less than the arithmetic mean.
Русский
Если хотя бы два значения z_i различны и веса положительны, неравенство АМ-ГМ строгое.
LaTeX
$$$\\prod_{i\\in s} z_i^{w_i} < \\sum_{i\\in s} w_i z_i \\;\\Leftrightarrow\\; \\exists j,k\\in s: z_j \\neq z_k$$$
Lean4
/-- **AM-GM inequality - strict inequality condition**: This theorem provides the strict inequality
condition for the *positive* weighted version of the AM-GM inequality for real-valued nonnegative
functions. -/
theorem geom_mean_lt_arith_mean_weighted_iff_of_pos (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, ∃ k ∈ s, z j ≠ z k :=
by
constructor
· intro h
by_contra! h_contra
rw [(geom_mean_eq_arith_mean_weighted_iff' s w z hw hw' hz).mpr ?_] at h
· exact (lt_self_iff_false _).mp h
· intro j hjs
rw [← arith_mean_weighted_of_constant s w (fun _ => z j) (z j) hw' fun _ _ => congrFun rfl]
apply sum_congr rfl (fun x a => congrArg (HMul.hMul (w x)) (h_contra j hjs x a))
· rintro ⟨j, hjs, k, hks, hzjk⟩
have := geom_mean_le_arith_mean_weighted s w z (fun i a => le_of_lt (hw i a)) hw' hz
by_contra! h
apply le_antisymm this at h
apply(geom_mean_eq_arith_mean_weighted_iff' s w z hw hw' hz).mp at h
simp only [h j hjs, h k hks, ne_eq, not_true_eq_false] at hzjk
