mathlib documentation

ring_theory.polynomial.hermite.basic

Hermite polynomials #

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_of_odd_add: for n,k where n+k is odd, (hermite n).coeff k is zero.
polynomial.monic_hermite: for all n, hermite n is monic.

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