rpow_arith_mean_le_arith_mean_rpow

English

For finite s and nonnegative w,z with sum w_i =1, the rpow mean bound holds: ∑ w_i z_i ≤ (∑ w_i z_i^p)^{1/p}.

Русский

Для конечного s, неотрицательных w,z с суммой 1: ∑ w_i z_i ≤ (∑ w_i z_i^p)^{1/p}.

LaTeX

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

Lean4

theorem rpow_arith_mean_le_arith_mean_rpow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1)
    (hz : ∀ i ∈ s, 0 ≤ z i) {p : ℝ} (hp : 1 ≤ p) : (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p :=
  (convexOn_rpow hp).map_sum_le hw hw' hz

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