pow_arith_mean_le_arith_mean_pow — Mathlib

English

For NNReal with s finite and p≥1, (∑ w_i z_i)^p ≤ ∑ w_i z_i^p.

Русский

Для NNReal: (∑ w_i z_i)^p ≤ ∑ w_i z_i^p при p≥1.

LaTeX

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

Lean4

/-- Weighted generalized mean inequality, version sums over finite sets, with `ℝ≥0`-valued
functions and natural exponent. -/
theorem pow_arith_mean_le_arith_mean_pow (w z : ι → ℝ≥0) (hw' : ∑ i ∈ s, w i = 1) (n : ℕ) :
    (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n :=
  mod_cast
    Real.pow_arith_mean_le_arith_mean_pow s _ _ (fun i _ => (w i).coe_nonneg) (mod_cast hw')
      (fun i _ => (z i).coe_nonneg) n

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