mathlib documentation

ring_theory.polynomial.hermite.basic

Hermite polynomials #

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)) :