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 : Nat → Polynomial Int

the probabilists' Hermite polynomials.

Equations

• Eq (Polynomial.hermite 0) 1
• Eq (Polynomial.hermite n.succ) (HSub.hSub (HMul.hMul Polynomial.X (Polynomial.hermite n)) (DFunLike.coe Polynomial.derivative (Polynomial.hermite n)))

theorem Polynomial.hermite_succ (n : Nat) : Eq (hermite (HAdd.hAdd n 1)) (HSub.hSub (HMul.hMul X (hermite n)) (DFunLike.coe derivative (hermite n)))

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

theorem Polynomial.hermite_eq_iterate (n : Nat) : Eq (hermite n) (Nat.iterate (fun (p : Polynomial Int) => HSub.hSub (HMul.hMul X p) (DFunLike.coe derivative p)) n 1)

theorem Polynomial.hermite_zero : Eq (hermite 0) (DFunLike.coe C 1)

theorem Polynomial.hermite_one : Eq (hermite 1) X

Lemmas about Polynomial.coeff

theorem Polynomial.coeff_hermite_succ_zero (n : Nat) : Eq ((hermite (HAdd.hAdd n 1)).coeff 0) (Neg.neg ((hermite n).coeff 1))

theorem Polynomial.coeff_hermite_succ_succ (n k : Nat) : Eq ((hermite (HAdd.hAdd n 1)).coeff (HAdd.hAdd k 1)) (HSub.hSub ((hermite n).coeff k) (HMul.hMul (HAdd.hAdd k.cast 2) ((hermite n).coeff (HAdd.hAdd k 2))))

theorem Polynomial.coeff_hermite_of_lt {n k : Nat} (hnk : LT.lt n k) : Eq ((hermite n).coeff k) 0

theorem Polynomial.coeff_hermite_self (n : Nat) : Eq ((hermite n).coeff n) 1

theorem Polynomial.degree_hermite (n : Nat) : Eq (hermite n).degree n.cast

theorem Polynomial.natDegree_hermite {n : Nat} : Eq (hermite n).natDegree n

theorem Polynomial.leadingCoeff_hermite (n : Nat) : Eq (hermite n).leadingCoeff 1

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

theorem Polynomial.coeff_hermite_of_odd_add {n k : Nat} (hnk : Odd (HAdd.hAdd n k)) : Eq ((hermite n).coeff k) 0

@[irreducible]

theorem Polynomial.coeff_hermite_explicit (n k : Nat) : Eq ((hermite (HAdd.hAdd (HMul.hMul 2 n) k)).coeff k) (HMul.hMul (HMul.hMul (HPow.hPow (-1) n) (HSub.hSub (HMul.hMul 2 n) 1).doubleFactorial.cast) ((HAdd.hAdd (HMul.hMul 2 n) k).choose k).cast)

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

theorem Polynomial.coeff_hermite_of_even_add {n k : Nat} (hnk : Even (HAdd.hAdd n k)) : Eq ((hermite n).coeff k) (HMul.hMul (HMul.hMul (HPow.hPow (-1) (HDiv.hDiv (HSub.hSub n k) 2)) (HSub.hSub (HSub.hSub n k) 1).doubleFactorial.cast) (n.choose k).cast)

theorem Polynomial.coeff_hermite (n k : Nat) : Eq ((hermite n).coeff k) (ite (Even (HAdd.hAdd n k)) (HMul.hMul (HMul.hMul (HPow.hPow (-1) (HDiv.hDiv (HSub.hSub n k) 2)) (HSub.hSub (HSub.hSub n k) 1).doubleFactorial.cast) (n.choose k).cast) 0)