rpow_arith_mean_le_arith_mean2_rpow

English

With two weighted ENNReal values w1, w2 summing to 1 and z1, z2, and p ≥ 1, we have (w1 z1 + w2 z2)^p ≤ w1 z1^p + w2 z2^p.

Русский

С двумя значениями ENNReal и весами w1,w2 суммой 1 и z1,z2, при p ≥ 1 выполняется (w1 z1 + w2 z2)^p ≤ w1 z1^p + w2 z2^p.

LaTeX

$$$\forall w_1,w_2,z_1,z_2:\, (w_1+w_2=1) \Rightarrow (w_1 z_1 + w_2 z_2)^p ≤ w_1 z_1^p + w_2 z_2^p \ (p ≥ 1)$$$

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]

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