English
For NNReal, sums over finite set with weights summing to 1, and p≥1, rpow-arith mean inequality holds.
Русский
Для NNReal: rpow-arith-mean неравенство на конечном наборе с весами, суммирующимися в 1, и p≥1.
LaTeX
$$$\text{pow/arith mean bound for NNReal}$$$
Lean4
theorem arith_mean_le_rpow_mean (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 ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p) :=
by
have : 0 < p := by positivity
rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
· exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp
all_goals
apply_rules [sum_nonneg, rpow_nonneg]
intro i hi
apply_rules [mul_nonneg, rpow_nonneg, hw i hi, hz i hi]
