English
Weighted HM-GM inequality: the harmonic mean is less than or equal to the geometric mean with positive weights.
Русский
Взвешенное HM-GM: гармоническая средняя не превышает геометрическую.
LaTeX
$$$\\left( \\sum_{i} w_i / z_i \\right)^{-1} \\le \\prod_{i} z_i^{w_i}$$$
Lean4
/-- **HM-GM inequality**: The harmonic mean is less than or equal to the geometric mean, weighted
version for real-valued nonnegative functions. -/
theorem harm_mean_le_geom_mean_weighted (w z : ι → ℝ) (hs : s.Nonempty) (hw : ∀ i ∈ s, 0 < w i) (hw' : ∑ i ∈ s, w i = 1)
(hz : ∀ i ∈ s, 0 < z i) : (∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i :=
by
have : ∏ i ∈ s, (1 / z) i ^ w i ≤ ∑ i ∈ s, w i * (1 / z) i :=
geom_mean_le_arith_mean_weighted s w (1 / z) (fun i hi ↦ le_of_lt (hw i hi)) hw'
(fun i hi ↦ one_div_nonneg.2 (le_of_lt (hz i hi)))
have p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i := prod_pos fun i hi => rpow_pos_of_pos (inv_pos.2 (hz i hi)) _
have s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹ := sum_pos (fun i hi => mul_pos (hw i hi) (inv_pos.2 (hz i hi))) hs
norm_num at this
rw [← inv_le_inv₀ s_pos p_pos] at this
apply le_trans this
have p_pos₂ : 0 < (∏ i ∈ s, (z i) ^ w i)⁻¹ := inv_pos.2 (prod_pos fun i hi => rpow_pos_of_pos ((hz i hi)) _)
rw [← inv_inv (∏ i ∈ s, z i ^ w i), inv_le_inv₀ p_pos p_pos₂, ← Finset.prod_inv_distrib]
gcongr
· exact fun i hi ↦ inv_nonneg.mpr (Real.rpow_nonneg (le_of_lt (hz i hi)) _)
· rw [Real.inv_rpow]; apply fun i hi ↦ le_of_lt (hz i hi); assumption
