Hermite polynomials

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

Main definitions

• Polynomial.hermite n: the nth probabilists' Hermite polynomial, defined recursively as a Polynomial ℤ

Results

• Polynomial.hermite_succ: the recursion hermite (n+1) = (x - d/dx) (hermite n)
• Polynomial.coeff_hermite_explicit: a closed formula for (nonvanishing) coefficients in terms of binomial coefficients and double factorials.
• Polynomial.coeff_hermite_of_odd_add: for n,k where n+k is odd, (hermite n).coeff k is zero.
• Polynomial.coeff_hermite_of_even_add: a closed formula for (hermite n).coeff k when n+k is even, equivalent to Polynomial.coeff_hermite_explicit.
• Polynomial.monic_hermite: for all n, hermite n is monic.
• Polynomial.degree_hermite: for all n, hermite n has degree n.

References

• Hermite Polynomials

noncomputable def Polynomial.hermite : ℕ → Polynomial ℤ

the probabilists' Hermite polynomials.

Equations

• Polynomial.hermite 0 = 1
• Polynomial.hermite n.succ = Polynomial.X * Polynomial.hermite n - Polynomial.derivative (Polynomial.hermite n)

@[simp]

theorem Polynomial.hermite_succ (n : ℕ) : Polynomial.hermite (n + 1) = Polynomial.X * Polynomial.hermite n - Polynomial.derivative (Polynomial.hermite n)

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

theorem Polynomial.hermite_eq_iterate (n : ℕ) : Polynomial.hermite n = (fun (p : Polynomial ℤ) => Polynomial.X * p - Polynomial.derivative p)^[n] 1

@[simp]

theorem Polynomial.hermite_zero : Polynomial.hermite 0 = Polynomial.C 1

theorem Polynomial.hermite_one : Polynomial.hermite 1 = Polynomial.X

Lemmas about Polynomial.coeff

theorem Polynomial.coeff_hermite_succ_zero (n : ℕ) : (Polynomial.hermite (n + 1)).coeff 0 = -(Polynomial.hermite n).coeff 1

theorem Polynomial.coeff_hermite_succ_succ (n : ℕ) (k : ℕ) : (Polynomial.hermite (n + 1)).coeff (k + 1) = (Polynomial.hermite n).coeff k - (↑k + 2) * (Polynomial.hermite n).coeff (k + 2)

theorem Polynomial.coeff_hermite_of_lt {n : ℕ} {k : ℕ} (hnk : n < k) : (Polynomial.hermite n).coeff k = 0

@[simp]

theorem Polynomial.coeff_hermite_self (n : ℕ) : (Polynomial.hermite n).coeff n = 1

@[simp]

theorem Polynomial.degree_hermite (n : ℕ) : (Polynomial.hermite n).degree = ↑n

@[simp]

theorem Polynomial.natDegree_hermite {n : ℕ} : (Polynomial.hermite n).natDegree = n

@[simp]

theorem Polynomial.leadingCoeff_hermite (n : ℕ) : (Polynomial.hermite n).leadingCoeff = 1

theorem Polynomial.hermite_monic (n : ℕ) : (Polynomial.hermite n).Monic

theorem Polynomial.coeff_hermite_of_odd_add {n : ℕ} {k : ℕ} (hnk : Odd (n + k)) : (Polynomial.hermite n).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)) : (Polynomial.hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1).doubleFactorial * ↑(n.choose k)

theorem Polynomial.coeff_hermite (n : ℕ) (k : ℕ) : (Polynomial.hermite n).coeff k = if Even (n + k) then (-1) ^ ((n - k) / 2) * ↑(n - k - 1).doubleFactorial * ↑(n.choose k) else 0