arith_mean_le_rpow_mean — Mathlib

English

In NNReal, for finite s with weights summing to 1 and real p, the powered mean inequality bounds the p-th power of the mean.

Русский

Для NNReal: неравенство для p-й степени среднего.

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 arith_mean_le_rpow_mean (w z : ι → ℝ≥0) (hw' : ∑ i ∈ s, w i = 1) {p : ℝ} (hp : 1 ≤ p) :
    ∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p) :=
  mod_cast
    Real.arith_mean_le_rpow_mean s _ _ (fun i _ => (w i).coe_nonneg) (mod_cast hw') (fun i _ => (z i).coe_nonneg) hp

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