rpow_arith_mean_le_arith_mean2_rpow

English

For NNReal finite two-element case with weights summing to 1, the rpow mean inequality holds for all p≥1.

Русский

Для двух элементов с весами, сумма которых равна 1, неравенство Холдерa верно.

LaTeX

$$$\bigl( w_1 z_1 + w_2 z_2 \bigr)^p \le w_1 z_1^p + w_2 z_2^p$$$

Lean4

/-- Weighted generalized mean inequality, version for two elements of `ℝ≥0` and real exponents. -/
theorem rpow_arith_mean_le_arith_mean2_rpow (w₁ w₂ z₁ z₂ : ℝ≥0) (hw' : w₁ + w₂ = 1) {p : ℝ} (hp : 1 ≤ p) :
    (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p :=
  by
  have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
  · simpa [Fin.sum_univ_succ] using h
  · simp [hw', Fin.sum_univ_succ]

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