English
On the interval [n−1, ∞), the value of (descPochhammer S n).eval s is bounded below by (s−n+1)^n.
Русский
На промежутке [n−1, ∞) значение (descPochhammer S n).eval s не меньше (s−n+1)^n.
LaTeX
$$$\\forall s\\ge n-1:\\, (s-n+1)^n \\le (\\operatorname{descPochhammer} \\, S\\, n).\\mathrm{eval}\\, s$$$
Lean4
/-- `descPochhammer S n` is at least `(s-n+1)^n` on `[n-1, ∞)`. -/
theorem pow_le_descPochhammer_eval {n : ℕ} {s : S} (h : n - 1 ≤ s) : (s - n + 1) ^ n ≤ (descPochhammer S n).eval s := by
induction n with
| zero => simp
| succ n ih =>
rw [Nat.cast_add_one, add_sub_cancel_right, ← sub_nonneg] at h
have hsub1 : n - 1 ≤ s := (sub_le_self (n : S) zero_le_one).trans (le_of_sub_nonneg h)
rw [pow_succ, descPochhammer_succ_eval, Nat.cast_add_one, sub_add, add_sub_cancel_right]
apply mul_le_mul _ le_rfl h (descPochhammer_nonneg hsub1)
exact (ih hsub1).trans' <| pow_le_pow_left₀ h (le_add_of_nonneg_right zero_le_one) n
