English
A Jensen-type inequality for Nat.choose: the eval at a convex combination is bounded by the convex combination of choose-values divided by n.
Русский
Неравенство Дженсен для выбора Нат: оценка в выпуклой комбинации ограничена выпуклой комбинацией значений choose по n.
LaTeX
$$$$ \frac{( \mathrm{descPochhammer} \mathbb{R} n).\mathrm{eval}}{n!.} \le \sum_{i \in t} w_i \ (p_i).\mathrm{choose} n. $$$$
Lean4
/-- Special case of **Jensen's inequality** for `Nat.choose`. -/
theorem descPochhammer_eval_div_factorial_le_sum_choose (hn : n ≠ 0) {ι : Type*} {t : Finset ι} (p : ι → ℕ) (w : ι → ℝ)
(h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (h_avg : n - 1 ≤ ∑ i ∈ t, w i * p i) :
(descPochhammer ℝ n).eval (∑ i ∈ t, w i * p i) / n.factorial ≤ ∑ i ∈ t, w i * (p i).choose n :=
by
simp_rw [Nat.cast_choose_eq_descPochhammer_div, mul_div, ← Finset.sum_div, descPochhammer_eval_eq_descFactorial]
apply div_le_div_of_nonneg_right _ (Nat.cast_nonneg n.factorial)
exact descPochhammer_eval_le_sum_descFactorial hn p w h₀ h₁ h_avg
