geom_mean_le_arith_mean2_weighted

English

Equality characterization for NNReal weighted AM-GM.

Русский

Условие равенства в NNReal-версии АМ-ГМ.

LaTeX

$$$\\text{Equality iff ... }$$$

Lean4

/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean, weighted
version for two `NNReal` numbers. -/
theorem geom_mean_le_arith_mean2_weighted (w₁ w₂ p₁ p₂ : ℝ≥0) :
    w₁ + w₂ = 1 → p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) ≤ w₁ * p₁ + w₂ * p₂ := by
  simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty, Finset.univ_eq_empty,
    Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂] ![p₁, p₂]

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