# Hermite polynomials #

This file defines Polynomial.hermite n, the nth probabilists' Hermite polynomial.

## References #

noncomputable def Polynomial.hermite :

the probabilists' Hermite polynomials.

Equations
Instances For
@[simp]
theorem Polynomial.hermite_succ (n : ) :
Polynomial.hermite (n + 1) = Polynomial.X * - Polynomial.derivative

The recursion hermite (n+1) = (x - d/dx) (hermite n)

theorem Polynomial.hermite_eq_iterate (n : ) :
= (fun (p : ) => Polynomial.X * p - Polynomial.derivative p)^[n] 1
@[simp]
theorem Polynomial.hermite_zero :
= Polynomial.C 1
theorem Polynomial.hermite_one :
= Polynomial.X

theorem Polynomial.coeff_hermite_succ_zero (n : ) :
(Polynomial.hermite (n + 1)).coeff 0 = -.coeff 1
theorem Polynomial.coeff_hermite_succ_succ (n : ) (k : ) :
(Polynomial.hermite (n + 1)).coeff (k + 1) = .coeff k - (k + 2) * .coeff (k + 2)
theorem Polynomial.coeff_hermite_of_lt {n : } {k : } (hnk : n < k) :
.coeff k = 0
@[simp]
theorem Polynomial.coeff_hermite_self (n : ) :
.coeff n = 1
@[simp]
theorem Polynomial.degree_hermite (n : ) :
.degree = n
@[simp]
theorem Polynomial.natDegree_hermite {n : } :
.natDegree = n
@[simp]
theorem Polynomial.leadingCoeff_hermite (n : ) :
theorem Polynomial.hermite_monic (n : ) :
.Monic
theorem Polynomial.coeff_hermite_of_odd_add {n : } {k : } (hnk : Odd (n + k)) :
.coeff k = 0
@[irreducible]
theorem Polynomial.coeff_hermite_explicit (n : ) (k : ) :
(Polynomial.hermite (2 * n + k)).coeff k = (-1) ^ n * (2 * n - 1).doubleFactorial * ((2 * n + k).choose k)

Because of coeff_hermite_of_odd_add, every nonzero coefficient is described as follows.

theorem Polynomial.coeff_hermite_of_even_add {n : } {k : } (hnk : Even (n + k)) :
.coeff k = (-1) ^ ((n - k) / 2) * (n - k - 1).doubleFactorial * (n.choose k)
theorem Polynomial.coeff_hermite (n : ) (k : ) :
.coeff k = if Even (n + k) then (-1) ^ ((n - k) / 2) * (n - k - 1).doubleFactorial * (n.choose k) else 0