pow_arith_mean_le_arith_mean_pow_of_even

English

If n is even and w_i≥0 with sum 1, then (∑ w_i z_i)^n ≤ ∑ w_i z_i^n.

Русский

Если n чётно, то аналогично неравенство для средних степеней.

LaTeX

$$$\left(\sum_{i\in s} w_i z_i\right)^n \le \sum_{i\in s} w_i z_i^n$, при n чётном$$

Lean4

theorem pow_arith_mean_le_arith_mean_pow_of_even (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) {n : ℕ}
    (hn : Even n) : (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n :=
  hn.convexOn_pow.map_sum_le hw hw' fun _ _ => Set.mem_univ _

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