English
The derivative of the eval map is monotone on the interval (n-1, ∞).
Русский
Производная отображения от eval монотонна на интервале (n-1, ∞).
LaTeX
$$$$ \operatorname{MonotoneOn}\big( \mathrm{deriv}\big( \mathrm{descPochhammer}(\mathbb{R}, n) \).\mathrm{eval} \big)\big( \mathrm{Ioi}(n-1) \big). $$$$
Lean4
/-- `deriv (descPochhammer ℝ n)` is monotone on `(n-1, ∞)`. -/
theorem monotoneOn_deriv_descPochhammer_eval (n : ℕ) :
MonotoneOn (deriv (descPochhammer ℝ n).eval) (Set.Ioi (n - 1 : ℝ)) := by
induction n with
| zero => simp [monotoneOn_const]
| succ n ih =>
intro a ha b hb hab
rw [Set.mem_Ioi, Nat.cast_add_one, add_sub_cancel_right] at ha hb
simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]
apply Finset.sum_le_sum; intro i hi
apply Finset.prod_le_prod
· intro j hj
rw [Finset.mem_erase, Finset.mem_range] at hj
apply sub_nonneg_of_le
exact ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)
· intro j hj
rwa [← sub_le_sub_iff_right (j : ℝ)] at hab
