zpow_arith_mean_le_arith_mean_zpow

English

For finite s, w_i≥0 with ∑ w_i = 1 and z_i≥0, for any p∈ℝ with 1≤p, (∑ w_i z_i)^p ≤ ∑ w_i z_i^p.

Русский

Для конечного s, неотрицательных w_i и z_i, с суммой 1, для любого p≥1: (∑ w_i z_i)^p ≤ ∑ w_i z_i^p.

LaTeX

$$$\left(\sum_{i\in s} w_i z_i\right)^p \le \sum_{i\in s} w_i z_i^p$$$

Lean4

theorem zpow_arith_mean_le_arith_mean_zpow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1)
    (hz : ∀ i ∈ s, 0 < z i) (m : ℤ) : (∑ i ∈ s, w i * z i) ^ m ≤ ∑ i ∈ s, w i * z i ^ m :=
  (convexOn_zpow m).map_sum_le hw hw' hz

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