English
For all n,k, coeff(hermite n) k equals (-1)^n (2n-1)‼ Nat.choose (2n+k) k if n+k even, and 0 otherwise.
Русский
Для всех n,k коэффициент Hermite n в k равен (-1)^n (2n-1)‼ C(2n+k, k) если n+k чётно, иначе 0.
LaTeX
$$$\operatorname{coeff}(\operatorname{hermite}(n),k) = \begin{cases}(-1)^n (2n-1)‼ \cdot \binom{2n+k}{k}, & \text{если } \operatorname{Even}(n+k) \\ 0, & \text{иначе} \end{cases}$$$
Lean4
/-- Because of `coeff_hermite_of_odd_add`, every nonzero coefficient is described as follows. -/
theorem coeff_hermite_explicit :
∀ n k : ℕ, coeff (hermite (2 * n + k)) k = (-1) ^ n * (2 * n - 1)‼ * Nat.choose (2 * n + k) k
| 0, _ => by simp
| n + 1, 0 => by
convert coeff_hermite_succ_zero (2 * n + 1) using 1
rw [coeff_hermite_explicit n 1, (by grind : 2 * (n + 1) - 1 = 2 * n + 1), Nat.doubleFactorial_add_one,
Nat.choose_zero_right, Nat.choose_one_right, pow_succ]
push_cast
ring
| n + 1, k + 1 =>
by
let hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * (2 * n - 1)‼ * Nat.choose (2 * n + k) k
have hermite_explicit_recur :
∀ n k : ℕ, hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (k + 2) * hermite_explicit n (k + 2) :=
by
intro n k
simp only [hermite_explicit]
-- Factor out (-1)'s.
rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
nth_rw 3 [neg_eq_neg_one_mul]
simp only [mul_assoc, ← mul_add, pow_succ']
congr 2
-- Factor out double factorials.
norm_cast
rw [(by grind : 2 * (n + 1) - 1 = 2 * n + 1), Nat.doubleFactorial_add_one, mul_comm (2 * n + 1)]
simp only [mul_assoc, ← mul_add]
congr 1
-- Match up binomial coefficients using `Nat.choose_succ_right_eq`.
rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1),
(by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)), (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel]
ring
change _ = hermite_explicit _ _
rw [← add_assoc, coeff_hermite_succ_succ, hermite_explicit_recur]
congr
· rw [coeff_hermite_explicit (n + 1) k]
· rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]
