geom_mean_le_arith_mean3_weighted

English

AM-GM for four NNReal numbers with weights summing to 1.

Русский

AM-GM для четырех NNReal чисел с суммой весов 1.

LaTeX

$$$\\prod_{i=1}^4 z_i^{w_i} \\le \\sum_{i=1}^4 w_i z_i$$$

Lean4

theorem geom_mean_le_arith_mean3_weighted (w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0) :
    w₁ + w₂ + w₃ = 1 → p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) * p₃ ^ (w₃ : ℝ) ≤ w₁ * p₁ + 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, ← add_assoc, mul_assoc] using
    geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃] ![p₁, p₂, p₃]

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