English
A Jensen-type inequality holds for Nat.descPochhammer: the descPochhammer evaluation at a weighted average is bounded by the weighted average of descFactorial values.
Русский
Для Nat.descPochhammer выполняется неравенство Дженсен: значение на взвешенном среднике не превосходит взвешенную сумму descFactorial.
LaTeX
$$$$ \text{Jensen: } (\mathrm{descPochhammer} \mathbb{R} n).\mathrm{eval}\Big( \sum_{i\in t} w_i p_i \Big) \le \sum_{i\in t} w_i \ (p_i).descFactorial n. $$$$
Lean4
/-- Special case of **Jensen's inequality** for `Nat.descFactorial`. -/
theorem descPochhammer_eval_le_sum_descFactorial (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) ≤ ∑ i ∈ t, w i * (p i).descFactorial n :=
by
let f : ℝ → ℝ := (Set.Ici (n - 1 : ℝ)).piecewise (descPochhammer ℝ n).eval 0
suffices h_jensen : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i) by
simpa only [smul_eq_mul, f, Set.piecewise_eq_of_mem (Set.Ici (n - 1 : ℝ)) _ _ h_avg,
piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial] using h_jensen
exact ConvexOn.map_sum_le (convexOn_piecewise_Ici_descPochhammer_eval_zero hn) h₀ h₁ (by simp)
