Hermite polynomials, Laguerre polynomials, and Fock states

Definition

wigner_states

by Lucas · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisorthogonal-polynomialsquantum-mechanics

Physicists' Hermite polynomials, ordinary Laguerre polynomials, and the normalized Fock states of the harmonic oscillator. The Hermite polynomials $H_m$ are defined by the recurrence $H_0 = 1$ , $H_1(x) = 2x$ , $H_{n+1}(x) = 2x\,H_n(x) - 2n\,H_{n-1}(x)$ ; the Laguerre polynomials $L_m$ by $L_0 = 1$ , $L_1(x) = 1-x$ , $(m+1)L_{m+1}(x) = (2m+1-x)L_m(x) - mL_{m-1}(x)$ . The $m$ -th normalized Hermite (Fock) wavefunction is

u_m(x) = (2^m m!)^{-1/2}\,\pi^{-1/4}\,H_m(x)\,e^{-x^2/2},

the $m$ -th number state $|m\rangle = (a^\dagger)^m/\sqrt{m!}\,|0\rangle$ of the quantum harmonic oscillator, in dimensionless units ( $\hbar = m = \omega = 1$ ).

Formalization Note The factor $(2^m m!)^{-1/2}$ makes the states $u_m$ orthonormal in $L^2(\mathbb{R})$ ; it is required for Groenewold's closed formula for the Wigner function of a Fock state. The source's displayed eigenfunctions $u_m(x) = \pi^{-1/4}H_m(x)e^{-x^2/2}$ omit this normalization, but its Fock-state formula is stated for the normalized number states.

Definition code

import Mathlib

namespace Wigner

/-- The m-th physicists' Hermite polynomial H_m, defined by the three-term
recurrence H_0 = 1, H_1 (x) = 2 * x,
H_{n+1} (x) = 2 * x * H_n (x) - 2 * n * H_{n-1} (x). -/
def hermiteP : ℕ → ℝ → ℝ
  | 0, _ => 1
  | 1, x => 2 * x
  | n + 2, x => 2 * x * hermiteP (n + 1) x - 2 * (n + 1) * hermiteP n x

/-- The m-th ordinary Laguerre polynomial L_m, defined by the three-term
recurrence L_0 = 1, L_1 (x) = 1 - x,
(m + 1) * L_{m+1} (x) = (2 * m + 1 - x) * L_m (x) - m * L_{m-1} (x). -/
noncomputable def laguerreL : ℕ → ℝ → ℝ
  | 0, _ => 1
  | 1, x => 1 - x
  | m + 2, x => ((2 * (m + 1) + 1 - x) * laguerreL (m + 1) x - (m + 1) * laguerreL m x) / (m + 2)

/-- The m-th normalized Hermite (Fock) wavefunction of the harmonic oscillator,
u_m (x) = (2^m * m!)^(-1/2) * pi^(-1/4) * H_m (x) * exp (-x^2 / 2). -/
noncomputable def fockState (m : ℕ) (x : ℝ) : ℂ :=
  (((Real.pi ^ (-(1 / 4 : ℝ)) * hermiteP m x * Real.exp (-(x ^ 2) / 2) /
      Real.sqrt ((2 : ℝ) ^ m * ((Nat.factorial m : ℕ) : ℝ))) : ℝ) : ℂ)

end Wigner

Source

Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), sections "Examples" (Groenewold formula and Hermite functions) and "Positivity of the function". https://en.wikipedia.org/wiki/Wigner_quasiprobability_distribution

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

The code declares three definitions in the namespace Wigner and proves nothing.

hermiteP is a function $\mathbb{N} \to \mathbb{R} \to \mathbb{R}$ defined by recursion on the first argument: hermiteP $0\,x = 1$ ; hermiteP $1\,x = 2x$ ; hermiteP $(n{+}2)\,x = 2x \cdot \mathrm{hermiteP}(n{+}1)(x) - 2(n{+}1) \cdot \mathrm{hermiteP}(n)(x)$ .
laguerreL is a function $\mathbb{N} \to \mathbb{R} \to \mathbb{R}$ : laguerreL $0\,x = 1$ ; laguerreL $1\,x = 1 - x$ ; laguerreL $(m{+}2)\,x = ((2(m{+}1)+1-x)\cdot\mathrm{laguerreL}(m{+}1)(x) - (m{+}1)\cdot\mathrm{laguerreL}(m)(x)) / (m+2)$ , ordinary real division.
fockState $m\,x$ is the complex number obtained from the real number $\pi^{-1/4} \cdot \mathrm{hermiteP}(m)(x) \cdot e^{-x^2/2} / \sqrt{2^m \cdot m!}$ , where $\pi^{-1/4}$ is a real power, the square root is the nonnegative real square root (a total function on $\mathbb{R}$ , with a junk value at negative arguments; here the argument $2^m m!$ is a positive natural number), and $m!$ is the factorial of $m$ .

All three are total functions; no hypotheses.

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph