English
For Odd(n+k), coeff(hermite n, k) equals a specific explicit product: (-1)^n (2n-1)‼ Nat.choose (2n+k) k.
Русский
При нечетной сумме n+k коэффициент Hermite n в k равен конкретному явному выражению: (-1)^n (2n-1)‼ Nat.choose (2n+k) k.
LaTeX
$$$\text{If }\operatorname{Odd}(n+k)\text{, then } \operatorname{coeff}(\operatorname{hermite}(n),k)=(-1)^n(2n-1)‼\cdot\binom{2n+k}{k}.$$$
Lean4
theorem coeff_hermite_of_odd_add {n k : ℕ} (hnk : Odd (n + k)) : coeff (hermite n) k = 0 := by
induction n generalizing k with
| zero =>
rw [zero_add k] at hnk
exact coeff_hermite_of_lt hnk.pos
| succ n ih =>
cases k with
| zero =>
rw [Nat.succ_add_eq_add_succ] at hnk
rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
| succ k =>
rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
· rwa [Nat.succ_add_eq_add_succ] at hnk
· rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
exact (Nat.odd_add.mp hnk).mpr even_two
