pow_arith_mean_le_arith_mean_pow — Mathlib

English

Let s be finite and w_i ≥ 0 with sum w_i = 1, z_i ≥ 0. Then for any n, (∑ w_i z_i)^n ≤ ∑ w_i z_i^n.

Русский

Пусть s конечен, w_i ≥ 0 и ∑ w_i = 1, z_i ≥ 0. Тогда для любого n: (∑ w_i z_i)^n ≤ ∑ w_i z_i^n.

LaTeX

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

Lean4

theorem pow_arith_mean_le_arith_mean_pow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1)
    (hz : ∀ i ∈ s, 0 ≤ z i) (n : ℕ) : (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n :=
  (convexOn_pow n).map_sum_le hw hw' hz

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