geom_mean_le_arith_mean4_weighted

English

Four-term weighted AM-GM inequality.

Русский

Четырехчленная взвешенная AM-GM.

LaTeX

$$$p_1^{w_1} p_2^{w_2} p_3^{w_3} p_4^{w_4} \\le w_1 p_1 + w_2 p_2 + w_3 p_3 + w_4 p_4$ with weights summing to 1$$

Lean4

theorem geom_mean_le_arith_mean4_weighted {w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hw₃ : 0 ≤ w₃)
    (hw₄ : 0 ≤ w₄) (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hp₃ : 0 ≤ p₃) (hp₄ : 0 ≤ p₄) (hw : w₁ + w₂ + w₃ + w₄ = 1) :
    p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ * p₄ ^ w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄ :=
  NNReal.geom_mean_le_arith_mean4_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨w₃, hw₃⟩ ⟨w₄, hw₄⟩ ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ ⟨p₃, hp₃⟩
      ⟨p₄, hp₄⟩ <|
    NNReal.coe_inj.1 <| by assumption

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