Hermite Functions and Nuclear Structure of Schwartz Space

Hermite functions ψₙ(x) = cₙ · Hₙ(x) · exp(-x²/2) form an orthonormal basis of L²(ℝ) that also lies in Schwartz space 𝓢(ℝ). The Schwartz seminorm ‖ψₙ‖_{k,m} grows polynomially in n, making the inclusion maps between Sobolev-Hermite levels Hilbert-Schmidt (and their compositions trace-class).

This file provides:

• Definitions of Hermite functions (1D and multi-dimensional)
• Key properties as axioms (L² orthonormality, Schwartz membership, seminorm bounds)
• These properties are sufficient to prove schwartz_nuclear (in DyninMityagin.lean)

The polynomial infrastructure is available in ../auto1/lean/SpecialFunctions/Hermite/Basic.lean (probabilist's Hermite polynomials with full algebraic proofs).

References

• Reed-Simon, "Methods of Modern Mathematical Physics" Vol. 1, §V.3
• Folland, "Harmonic Analysis in Phase Space", Ch. 1
• Thangavelu, "Lectures on Hermite and Laguerre Expansions"
• DLMF Chapter 18 (Orthogonal Polynomials)

Hermite Functions (1D)

The n-th Hermite function is: ψₙ(x) = (n! √π)^{-1/2} · Hₙ(x√2) · exp(-x²/2) where Hₙ is the probabilist's Hermite polynomial (Mathlib's hermite n), evaluated at x√2 to give the standard physicist's normalization.

This is equivalent to the physicist's convention: ψₙ(x) = (2ⁿ n! √π)^{-1/2} · Heₙ(x) · exp(-x²/2) where Heₙ(x) = 2^{n/2} Hₙ(x√2) is the physicist's Hermite polynomial.

Key properties:

1. {ψₙ} forms an ONB of L²(ℝ)
2. Each ψₙ ∈ 𝓢(ℝ, ℝ) (Schwartz function)
3. ψₙ is an eigenfunction of the Fourier transform: ℱψₙ = (-i)ⁿ ψₙ
4. ψₙ is an eigenfunction of the harmonic oscillator: (-d²/dx² + x²)ψₙ = (2n+1)ψₙ

noncomputable def hermiteFunctionNormConst (n : ℕ) : ℝ

Normalization constant for the n-th Hermite function: cₙ = (n! · √π)^{-1/2}

Equations

• hermiteFunctionNormConst n = √(↑n.factorial * √Real.pi)⁻¹

noncomputable def hermiteFunction (n : ℕ) (x : ℝ) : ℝ

The n-th Hermite function ψₙ(x) = cₙ · Hₙ(x√2) · exp(-x²/2) where Hₙ is the probabilist's Hermite polynomial evaluated at x√2.

Equations

• hermiteFunction n x = hermiteFunctionNormConst n * Polynomial.eval (x * √2) (Polynomial.map (Int.castRingHom ℝ) (Polynomial.hermite n)) * Real.exp (-x ^ 2 / 2)

Key Properties (axioms — to be proved from Gaussian integral theory)

These are standard results from harmonic analysis. Proofs require:

• Gaussian integration: ∫ x^k exp(-x²) dx (partially in Mathlib)
• Recurrence-based orthogonality
• Schwartz space membership via polynomial bounds on derivatives

The polynomial algebraic infrastructure is available in auto1/lean/SpecialFunctions/Hermite/.

theorem hermiteFunction_memLp (n : ℕ) : MeasureTheory.MemLp (hermiteFunction n) 2 MeasureTheory.volume

Hermite functions are square-integrable.

Orthonormality proof infrastructure

We prove hermiteFunction_orthonormal via the IBP recurrence for J(n, m) = ∫ Hₙ(x) · Hₘ(x) · exp(-x²/2) dx, where Hₙ = hermite n (probabilist's). Key identity: J(n, m+1) = n · J(n-1, m), giving J(n,m) = δₙₘ · n! · √(2π).

@[reducible, inline]

noncomputable abbrev hermiteR (n : ℕ) : Polynomial ℝ

Abbreviation: Hermite polynomial evaluated over ℝ.

Equations

• hermiteR n = Polynomial.map (Int.castRingHom ℝ) (Polynomial.hermite n)

theorem hermite_derivative (n : ℕ) : Polynomial.derivative (Polynomial.hermite (n + 1)) = ↑(n + 1) * Polynomial.hermite n

The derivative of the (n+1)-th Hermite polynomial is (n+1) times the n-th. Adapted from auto1's probHermite_derivative.

@[reducible, inline]

noncomputable abbrev gaussian (x : ℝ) : ℝ

The unnormalized Gaussian weight exp(-x²/2) (no 1/√(2π) factor).

Equations

• gaussian x = Real.exp (-(x ^ 2 / 2))

noncomputable def J (n m : ℕ) : ℝ

The J integral: ∫ Hₙ(x) · Hₘ(x) · exp(-x²/2) dx.

Equations

• J n m = ∫ (x : ℝ), Polynomial.eval x (hermiteR n) * (Polynomial.eval x (hermiteR m) * gaussian x)

theorem J_eq (m n : ℕ) : J n m = if n = m then ↑n.factorial * √(2 * Real.pi) else 0

J(n, m) = if n = m then n! * √(2π) else 0.

theorem hermiteFunction_orthonormal (n m : ℕ) : ∫ (x : ℝ), hermiteFunction n x * hermiteFunction m x = if n = m then 1 else 0

Hermite functions are orthonormal in L²(ℝ): ∫ ψₙ(x) ψₘ(x) dx = δₙₘ

noncomputable def gaussianSchwartz : SchwartzMap ℝ ℝ

The Gaussian exp(-x²/2) as a Schwartz function.

Equations

• gaussianSchwartz = { toFun := fun (x : ℝ) => Real.exp (-(x ^ 2 / 2)), smooth' := gaussianSchwartz._proof_1, decay' := gaussianSchwartz._proof_2 }

theorem hermiteFunction_schwartz (n : ℕ) : ∃ (φ : SchwartzMap ℝ ℝ), ∀ (x : ℝ), φ x = hermiteFunction n x

Each Hermite function is a Schwartz function.

Raising/Lowering Operators and Seminorm Bounds

We prove polynomial growth of Schwartz seminorms via:

1. Raising/lowering operator identities for Hermite functions
2. L² norm bounds from orthonormality
3. Agmon (Sobolev) inequality: ‖f‖_∞² ≤ 2‖f‖₂·‖f'‖₂
4. Assembly: seminorm ≤ C·(1+n)^s

theorem hermite_X_mul (n : ℕ) : Polynomial.X * Polynomial.hermite (n + 1) = Polynomial.hermite (n + 2) + ↑(n + 1) * Polynomial.hermite n

X · Hₙ₊₁ = Hₙ₊₂ + (n+1) · Hₙ in ℤ[X].

theorem hermiteR_recurrence_succ (n : ℕ) (t : ℝ) : t * Polynomial.eval t (hermiteR (n + 1)) = Polynomial.eval t (hermiteR (n + 2)) + ↑(n + 1) * Polynomial.eval t (hermiteR n)

theorem hermiteR_recurrence_zero (t : ℝ) : t * Polynomial.eval t (hermiteR 0) = Polynomial.eval t (hermiteR 1)

Hermite recurrence for n = 0: t · H₀(t) = H₁(t).

theorem mul_x_hermiteFunction (n : ℕ) (x : ℝ) : x * hermiteFunction n x = √(↑(n + 1) / 2) * hermiteFunction (n + 1) x + √(↑n / 2) * hermiteFunction (n - 1) x

Multiplication by x: x·ψₙ = √((n+1)/2)·ψ_{n+1} + √(n/2)·ψ_{n-1}.

theorem hermiteFunction_contDiff (j m : ℕ) : ContDiff ℝ (↑m) (hermiteFunction j)

Hermite functions are smooth (ContDiff ℝ ⊤).

theorem deriv_hermiteFunction (n : ℕ) (x : ℝ) : deriv (hermiteFunction n) x = √(↑n / 2) * hermiteFunction (n - 1) x - √(↑(n + 1) / 2) * hermiteFunction (n + 1) x

Derivative identity: ψₙ'(x) = √(n/2) ψ_{n-1}(x) - √((n+1)/2) ψ_{n+1}(x). Proved from the product rule on cₙ · Hₙ(x√2) · exp(-x²/2) and Hermite recurrence.

theorem hermiteFunction_sup_bound : ∃ (C : ℝ) (s : ℝ), 0 < C ∧ 0 ≤ s ∧ ∀ (n : ℕ) (x : ℝ), |hermiteFunction n x| ≤ C * (1 + ↑n) ^ s

Agmon-type sup bound: |ψₙ(x)| grows at most polynomially in n. Uses FTC + Cauchy-Schwarz + orthonormality + derivative identity: |ψₙ(x)|² ≤ 2‖ψₙ‖₂ · ‖ψₙ'‖₂ = 2√((2n+1)/2) ≤ C·(1+n)^{1/2}.

theorem hermiteFunction_seminorm_bound (k m : ℕ) : ∃ (C : ℝ) (s : ℝ), 0 < C ∧ 0 ≤ s ∧ ∀ (n : ℕ), (SchwartzMap.seminorm ℝ k m) (Classical.choose ⋯) ≤ C * (1 + ↑n) ^ s

Schwartz seminorm bound: ‖ψₙ‖{k,m} grows at most polynomially in n. Specifically, there exist constants C, s depending on k, m such that ‖ψₙ‖{k,m} ≤ C · (1 + n)^s.

This is the key property ensuring that the inclusion between Sobolev-Hermite levels is Hilbert-Schmidt. The exponent s depends on the seminorm order: for the Schwartz seminorm p_{k,m}(f) = sup_x (1+|x|)^k |f^(m)(x)|, we have ‖ψₙ‖{k,m} ≤ C{k,m} · (1+n)^{(k+m)/2 + 1/4}.

Sobolev-Hermite Spaces

Using the Hermite expansion f = ∑ₙ cₙ ψₙ (where cₙ = ∫ f ψₙ), the Sobolev-Hermite space of order s is: Hˢ = { f : ∑ₙ (1+n)^{2s} |cₙ|² < ∞ }

The inclusion Hˢ⁺¹ ↪ Hˢ is diagonal with eigenvalues (1+n)^{-1}, and ∑ₙ (1+n)^{-2} = π²/6 < ∞, so each inclusion is Hilbert-Schmidt.

The Schwartz space equals ∩ₛ Hˢ, and the Schwartz topology is generated by the Sobolev-Hermite norms.

theorem sobolevHermite_hs_sum_bound (s : ℝ) (hs : 1 / 2 < s) : ∃ (C : ℝ), ∀ (N : ℕ), ∑ i ∈ Finset.range N, (1 + ↑i) ^ (-2 * s) ≤ C

The Hilbert-Schmidt sum for the inclusion between Sobolev-Hermite levels: ∑_{n=0}^{N-1} (1+n)^{-2s} is bounded for s > 1/2, uniformly in N.

Proof of Hermite completeness

We now prove hermiteFunction_complete (stated as an axiom above). Phase 1: Show ∫ f·xᵏ·exp(-x²/2) = 0 using the mul_x_hermiteFunction recurrence. Phase 2-3: Conclude f = 0 via Schwartz density in L².

theorem hermiteFunction_complete (f : ℝ → ℝ) : MeasureTheory.MemLp f 2 MeasureTheory.volume → (∀ (n : ℕ), ∫ (x : ℝ), f x * hermiteFunction n x = 0) → f =ᵐ[MeasureTheory.volume] 0

Hermite functions form a complete system in L²(ℝ): if ∫ f ψₙ = 0 for all n, then f = 0 a.e.

Multi-dimensional Hermite Functions

For ℝᵈ, Hermite functions are tensor products: Ψ_α(x) = ∏ᵢ ψ_{αᵢ}(xᵢ) for multi-index α = (α₁, ..., αd)

These form an ONB of L²(ℝᵈ) and lie in 𝓢(ℝᵈ, ℝ).

Schwartz Hermite Expansion (General D, F)

The 5 Hermite infrastructure definitions and theorems (basis, coefficients, expansion, seminorm growth, coefficient decay) are now proved in HermiteTensorProduct.lean via multi-dimensional tensor products of 1D Hermite functions.

The previous axiom declarations have been removed. Import HermiteTensorProduct to access schwartzHermiteBasis, schwartzHermiteCoeff, schwartz_hermite_expansion, schwartz_hermite_seminorm_growth, and schwartz_hermite_coefficient_decay.