Documentation

Mathlib.RingTheory.Polynomial.Hermite.Basic

Hermite polynomials #

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

Main definitions #

Results #

References #

noncomputable def Polynomial.hermite :

the probabilists' Hermite polynomials.

Equations
Instances For
    @[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

    Lemmas about Polynomial.coeff #

    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]
    @[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.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