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 (Nat.succ n) = 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.coeff (Polynomial.hermite (n + 1)) 0 = -Polynomial.coeff (Polynomial.hermite n) 1

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Polynomial.coeff_hermite_of_odd_add {n : ℕ} {k : ℕ} (hnk : Odd (n + k)) : Polynomial.coeff (Polynomial.hermite n) k = 0

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

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