coeff_hermite — Mathlib

English

For all n,k, coeff(hermite n) k equals the piecewise expression depending on whether n+k is even or odd.

Русский

Для всех n,k коэффициент Hermite n в k равен соответствующему разрезённому выражению в зависимости от чётности суммы n+k.

LaTeX

$$$\operatorname{coeff}(\operatorname{hermite}(n),k) = \begin{cases} (-1)^((n-k)/2) (n-k-1)‼ \cdot \binom{n}{k} & \text{если } \operatorname{Even}(n+k) \\ 0 & \text{если } \operatorname{Odd}(n+k) \end{cases}$$$

Lean4

theorem coeff_hermite (n k : ℕ) :
    coeff (hermite n) k = if Even (n + k) then (-1 : ℤ) ^ ((n - k) / 2) * (n - k - 1)‼ * Nat.choose n k else 0 :=
  by
  split_ifs with h
  · exact coeff_hermite_of_even_add h
  · exact coeff_hermite_of_odd_add (Nat.not_even_iff_odd.1 h)

Похожие утверждения