geom_mean_le_arith_mean4_weighted

English

Equality for four-term NNReal AM-GM.

Русский

Равенство в четырехчленном случае NNReal AM-GM.

LaTeX

$$$\\text{Equality for four terms under weights}$$$

Lean4

theorem geom_mean_le_arith_mean4_weighted (w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0) :
    w₁ + w₂ + w₃ + w₄ = 1 →
      p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) * p₃ ^ (w₃ : ℝ) * p₄ ^ (w₄ : ℝ) ≤ w₁ * p₁ + 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₃, w₄] ![p₁, p₂, p₃, p₄]

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