rpow_arith_mean_le_arith_mean_rpow

English

For finite s and NNReal w,z with sum w_i = 1, and any p, 1≤p implies the bound (∑ w_i z_i)^p ≤ ∑ w_i z_i^p.

Русский

Для NNReal: при конечном s и весах сумма 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 for sums over finite sets, with `ℝ≥0`-valued
functions and real exponents. -/
theorem rpow_arith_mean_le_arith_mean_rpow (w z : ι → ℝ≥0) (hw' : ∑ i ∈ s, w i = 1) {p : ℝ} (hp : 1 ≤ p) :
    (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p :=
  mod_cast
    Real.rpow_arith_mean_le_arith_mean_rpow s _ _ (fun i _ => (w i).coe_nonneg) (mod_cast hw')
      (fun i _ => (z i).coe_nonneg) hp

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