Families
Hermite polynomials
The probabilists' Hermite polynomials satisfy $H_0 = 1$, $H_1 = x$ and
$$H_{n+2}(x) = x\, H_{n+1}(x) - (n+1)\, H_n(x).$$
The following hold:
- each $H_n$ is monic of degree $n$, with only real and simple zeros;
- consecutive polynomials strictly interlace, and $H_n, H_{n-1}, \dotsc, H_0$ is a Sturm sequence;
- the recurrence is a Favard recurrence with diagonal $0$ and subdiagonal $n$;
- the polynomials are orthogonal for the Gaussian weight:
$$\int_{-\infty}^{\infty} H_i(x) H_j(x)\, e^{-x^2/2}\, dx = \delta_{ij} \sqrt{2\pi}\, i!.$$
The root and interlacing statements follow from the general Favard theory, because the subdiagonal is positive.
References
G. Szegő, Orthogonal Polynomials, American Mathematical Society Colloquium Publications 23 (1939).
≔ Definitions
Probabilists' Hermite polynomials
abbrev hermiteReal (n : ℕ) : ℝ[X] :=
(Polynomial.hermite n).map (Int.castRingHom ℝ)
Gaussian weight
def hermiteGaussianWeight (x : ℝ) : ℝ :=
Real.exp (-(x ^ 2 / 2))
⊢ Theorems
Hermite polynomials are real-rootedMain result
theorem hermiteReal_isRealRooted (n : ℕ) :
hermiteReal n ≠ 0 ∧ (hermiteReal n).Splits
Hermite polynomials have simple roots
theorem hermiteReal_hasSimpleRoots (n : ℕ) :
HasSimpleRoots (hermiteReal n)
Consecutive Hermite polynomials interlace
theorem hermiteReal_strictInterl_succ (n : ℕ) :
StrictInterl (hermiteReal n) (hermiteReal (n + 1))
Hermite polynomials form a Sturm sequence
theorem hermiteReal_isSturmSeq (n : ℕ) :
IsSturmSeq ((List.range (n + 1)).reverse.map hermiteReal)
Hermite polynomials satisfy a Favard recurrence
theorem hermiteReal_satisfiesFavardRecurrence :
SatisfiesFavardRecurrence hermiteReal
(fun _ ↦ (0 : ℝ)) (fun n ↦ (n : ℝ))
Hermite polynomials are orthogonal for the Gaussian weight
theorem hermiteReal_integral_orthogonal (i j : ℕ) :
(∫ x : ℝ,
(hermiteReal i).eval x * (hermiteReal j).eval x *
hermiteGaussianWeight x) =
if i = j then
Real.sqrt (2 * Real.pi) * (i.factorial : ℝ)
else 0
Lean source RealRooted/Challenges/HermitePolynomials.lean at revision 5827550b.