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 #

Results #

References #

noncomputable def polynomial.hermite  :

the nth probabilist's Hermite polynomial

Equations
@[simp]

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

Lemmas about polynomial.coeff #

theorem polynomial.coeff_hermite_of_lt {n k : } (hnk : n < k) :
theorem polynomial.coeff_hermite_of_odd_add {n k : } (hnk : odd (n + k)) :
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