English
Equality condition for HM-GM: the harmonic mean is equal to the geometric mean when certain proportional relations hold.
Русский
Условие равенства HM-GM: гармоническая равна геометрической средне, если выполняются пропорциональные условия.
LaTeX
$$$$\\text{Equality characterized by } \\cdots$$$$
Lean4
/-- **HM-GM inequality**: The **harmonic mean is less than or equal to the geometric mean. -/
theorem harm_mean_le_geom_mean {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (w : ι → ℝ) (z : ι → ℝ)
(hw : ∀ i ∈ s, 0 < w i) (hw' : 0 < ∑ i ∈ s, w i) (hz : ∀ i ∈ s, 0 < z i) :
(∑ i ∈ s, w i) / (∑ i ∈ s, w i / z i) ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ :=
by
have := harm_mean_le_geom_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z hs ?_ ?_ hz
· simp only at this
set n := ∑ i ∈ s, w i
nth_rw 1 [div_eq_mul_inv, (show n = (n⁻¹)⁻¹ by simp), ← mul_inv, Finset.mul_sum _ _ n⁻¹]
simp_rw [inv_mul_eq_div n ((w _) / (z _)), div_right_comm _ _ n]
convert this
rw [← Real.finset_prod_rpow s _ (fun i hi ↦ Real.rpow_nonneg (le_of_lt <| hz i hi) _)]
refine Finset.prod_congr rfl (fun i hi => ?_)
rw [← Real.rpow_mul (le_of_lt <| hz i hi) (w _) n⁻¹, div_eq_mul_inv (w _) n]
· exact fun i hi ↦ div_pos (hw i hi) hw'
· simp_rw [div_eq_mul_inv (w _) (∑ i ∈ s, w i), ← Finset.sum_mul _ _ (∑ i ∈ s, w i)⁻¹]
exact mul_inv_cancel₀ hw'.ne'
