geom_mean_le_arith_mean3_weighted

English

Three-term weighted AM-GM for Real numbers.

Русский

Трехчленная взвешенная AM-GM.

LaTeX

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

Lean4

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

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