geom_mean_le_arith_mean_weighted — Mathlib

English

Weighted AM-GM holds for NNReal-valued functions, using the real-valued version by casting.

Русский

AM-GM справедливо и для NNReal значений, через приведение к вещественному виду.

LaTeX

$$$\\prod_{i\\in s} z_i^{(w_i)} \\le \\sum_{i\\in s} w_i z_i$$$

Lean4

/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean, weighted
version for `NNReal`-valued functions. -/
theorem geom_mean_le_arith_mean_weighted (w z : ι → ℝ≥0) (hw' : ∑ i ∈ s, w i = 1) :
    (∏ i ∈ s, z i ^ (w i : ℝ)) ≤ ∑ i ∈ s, w i * z i :=
  mod_cast
    Real.geom_mean_le_arith_mean_weighted _ _ _ (fun i _ => (w i).coe_nonneg) (by assumption_mod_cast) fun i _ =>
      (z i).coe_nonneg

Похожие утверждения