mathlib3 documentation

ring_theory.polynomial.hermite.basic

Hermite polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines polynomial.hermite n, the nth probabilist's Hermite polynomial.

Main definitions #

polynomial.hermite n: the nth probabilist's 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 nth probabilist's Hermite polynomial

Equations

polynomial.hermite (n + 1) = polynomial.X * polynomial.hermite n - ⇑polynomial.derivative (polynomial.hermite n)
polynomial.hermite 0 = 1

@[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 = (λ (p : polynomial ℤ), polynomial.X * p - ⇑polynomial.derivative p)^[n] 1

@[simp]

theorem polynomial.hermite_zero :

polynomial.hermite 0 = ⇑polynomial.C 1

@[simp]

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.nat_degree_hermite {n : ℕ} :

(polynomial.hermite n).nat_degree = n

@[simp]

theorem polynomial.leading_coeff_hermite (n : ℕ) :

(polynomial.hermite n).leading_coeff = 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

theorem polynomial.coeff_hermite_explicit (n k : ℕ) :

(polynomial.hermite (2 * n + k)).coeff k = (-1) ^ n * ↑((2 * n - 1).double_factorial) * ↑((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).double_factorial) * ↑(n.choose k)

theorem polynomial.coeff_hermite (n k : ℕ) :

(polynomial.hermite n).coeff k = ite (even (n + k)) ((-1) ^ ((n - k) / 2) * ↑((n - k - 1).double_factorial) * ↑(n.choose k)) 0