English
For each n, the function x ↦ (descPochhammer S n).eval x is monotone on the interval [n−1, ∞).
Русский
Для каждого n функция x ↦ (descPochhammer S n).eval x монотонна на окрестности [n−1, ∞).
LaTeX
$$$\\text{MonotoneOn}\\Bigl((\\operatorname{descPochhammer} \\ S\\, n).\\mathrm{eval},\, \\mathrm{Set.Ici}(n-1)\\Bigr)$$$
Lean4
/-- `descPochhammer S n` is monotone on `[n-1, ∞)`. -/
theorem monotoneOn_descPochhammer_eval (n : ℕ) : MonotoneOn (descPochhammer S n).eval (Set.Ici (n - 1 : S)) := by
induction n with
| zero => simp [monotoneOn_const]
| succ n ih =>
intro a ha b hb hab
rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb
have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
simp_rw [descPochhammer_succ_eval]
exact
mul_le_mul (ih ha_sub1 hb_sub1 hab) (sub_le_sub_right hab (n : S)) (sub_nonneg_of_le ha)
(descPochhammer_nonneg hb_sub1)
