English
For nonnegative infinite-valued weights w_i and nonnegative z_i with total weight 1, and p ≥ 1, we have (sum w_i z_i)^p ≤ sum w_i z_i^p.
Русский
Для ненулевых весов w_i и значений z_i в ℝ≥0∞ с суммой 1 и p ≥ 1 выполняется (∑ w_i z_i)^p ≤ ∑ w_i z_i^p.
LaTeX
$$$\forall s:\ Finset,\forall w,z:\,s \to ℝ_{≥0,∞},\ (\sum_{i∈s} w_i) = 1 \Rightarrow (\sum_{i∈s} w_i z_i)^p \le \sum_{i∈s} w_i z_i^p \ (p ≥ 1)$$$
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 :=
by
have hp_pos : 0 < p := by positivity
have hp_nonneg : 0 ≤ p := by positivity
have hp_not_neg : ¬p < 0 := by simp [hp_nonneg]
have h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤) := by
simp [ENNReal.mul_eq_top, hp_pos, hp_not_neg]
refine le_of_top_imp_top_of_toNNReal_le ?_ ?_
· -- first, prove `(∑ i ∈ s, w i * z i) ^ p = ⊤ → ∑ i ∈ s, (w i * z i ^ p) = ⊤`
rw [rpow_eq_top_iff, sum_eq_top, sum_eq_top]
grind
· -- second, suppose both `(∑ i ∈ s, w i * z i) ^ p ≠ ⊤` and `∑ i ∈ s, (w i * z i ^ p) ≠ ⊤`,
-- and prove `((∑ i ∈ s, w i * z i) ^ p).toNNReal ≤ (∑ i ∈ s, (w i * z i ^ p)).toNNReal`,
-- by using `NNReal.rpow_arith_mean_le_arith_mean_rpow`.
intro h_top_rpow_sum
_
-- show hypotheses needed to put the `.toNNReal` inside the sums.
have h_top : ∀ a : ι, a ∈ s → w a * z a ≠ ⊤ :=
haveI h_top_sum : ∑ i ∈ s, w i * z i ≠ ⊤ := by
intro h
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
exact h_top_rpow_sum rfl
fun a ha => (lt_top_of_sum_ne_top h_top_sum ha).ne
have h_top_rpow : ∀ a : ι, a ∈ s → w a * z a ^ p ≠ ⊤ :=
by
intro i hi
specialize h_top i hi
rwa [Ne, ← h_top_iff_rpow_top i hi]
-- put the `.toNNReal` inside the sums.
simp_rw [toNNReal_sum h_top_rpow, toNNReal_rpow, toNNReal_sum h_top, toNNReal_mul, toNNReal_rpow]
-- use corresponding nnreal result
refine NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal) (fun i => (z i).toNNReal) ?_ hp
have h_sum_nnreal : ∑ i ∈ s, w i = ↑(∑ i ∈ s, (w i).toNNReal) :=
by
rw [coe_finset_sum]
refine sum_congr rfl fun i hi => (coe_toNNReal ?_).symm
refine (lt_top_of_sum_ne_top ?_ hi).ne
exact hw'.symm ▸ ENNReal.one_ne_top
rwa [← coe_inj, ← h_sum_nnreal]
