The Hermite functions diagonalize the Fourier transform of L²(ℝ)

TauCeti.fourier_twoPiHermiteFunction computes the Fourier integral of the rescaled Hermite function Φₙ(x) = √(√(2π)) ψₙ(√(2π)x), the family adapted to Mathlib's e^{-2πixξ} convention: 𝓕 Φₙ = (-i)ⁿ Φₙ. That is a statement about one function at a time. This file turns it into a statement about the operator: Φₙ is a Hilbert basis of L²(ℝ), and Mathlib's unitary Fourier transform MeasureTheory.Lp.fourierTransformₗᵢ is diagonal in it, with eigenvalue (-i)ⁿ on the n-th vector. Every L² function therefore has its Fourier transform given by the termwise rescaling of its Hermite expansion, and the fourth iterate of the transform is the identity.

The basis is assembled by the roadmap's family-agnostic bridge TauCeti.hilbertBasisOfOrthogonalSystem, exactly as TauCeti.hermiteHilbertBasis is, but at the Fourier-adapted data: the weight w(x) = e^{-2πx²}, whose envelope √w(x) = e^{-πx²} is the self-dual Gaussian of Mathlib's convention, the exact-degree polynomials Hₙ(2√π·x), and the normalization cₙ = n!√π/√(2π). Completeness is the same moment-determinacy mechanism, since a Gaussian weight of any width has finite exponential moments.

Main statements

• TauCeti.twoPiHermiteHilbertBasis — the rescaled Hermite functions as a HilbertBasis ℕ 𝕜 of L²(ℝ), for every RCLike scalar field 𝕜, with the element-level TauCeti.coe_twoPiHermiteHilbertBasis.
• TauCeti.fourier_twoPiHermiteFunctionLp — the eigenrelation 𝓕 Φₙ = (-i)ⁿ Φₙ for the unitary Fourier transform of L²(ℝ; ℂ).
• TauCeti.hasSum_fourier_twoPiHermiteFunctionLp — the diagonalization: the Fourier transform of an arbitrary f ∈ L²(ℝ; ℂ) is its Hermite expansion with the n-th coefficient multiplied by (-i)ⁿ; TauCeti.repr_fourier_twoPiHermiteHilbertBasis is the same fact read on the coefficients.
• TauCeti.fourier_fourier_fourier_fourier — the fourth iterate of the Fourier transform of L²(ℝ; ℂ) is the identity.

References

• G. B. Folland, Harmonic Analysis in Phase Space, §1.

The Fourier-adapted Hermite system

noncomputable def TauCeti.twoPiHermiteDilated (n : ℕ) : Polynomial ℝ

The Hermite polynomial dilated to Mathlib's Fourier convention, Hₙ(2√π · X). Its Gaussian envelope e^{-πx²} is the self-dual Gaussian of the e^{-2πixξ} convention, so the resulting √w-normalized functions are the TauCeti.twoPiHermiteFunction.

Equations

• TauCeti.twoPiHermiteDilated n = (TauCeti.hermiteDilated n).comp (Polynomial.C √(2 * Real.pi) * Polynomial.X)

theorem TauCeti.eval_twoPiHermiteDilated (n : ℕ) (x : ℝ) : Polynomial.eval x (twoPiHermiteDilated n) = Polynomial.eval (√(2 * Real.pi) * x) (hermiteDilated n)

Evaluating TauCeti.twoPiHermiteDilated is evaluating TauCeti.hermiteDilated at the rescaled argument √(2π)·x.

theorem TauCeti.degree_twoPiHermiteDilated (n : ℕ) : (twoPiHermiteDilated n).degree = ↑n

The Fourier dilation preserves degrees, the input the completeness argument needs.

noncomputable def TauCeti.twoPiHermiteNormalization (n : ℕ) : ℝ

The normalization cₙ = n!√π/√(2π) of the Fourier-adapted Hermite system: it is the Hermite normalization n!√π divided by the Jacobian √(2π) of the dilation u = √(2π)·x.

Equations

• TauCeti.twoPiHermiteNormalization n = ↑n.factorial * √Real.pi / √(2 * Real.pi)

theorem TauCeti.twoPiHermiteNormalization_pos (n : ℕ) : 0 < twoPiHermiteNormalization n

The Fourier-adapted normalization is positive, as the bridge requires.

theorem TauCeti.twoPiHermiteFunction_eq_eval_mul_exp (n : ℕ) (x : ℝ) : twoPiHermiteFunction n x = Polynomial.eval x (twoPiHermiteDilated n) * Real.exp (-(Real.pi * x ^ 2)) / √(twoPiHermiteNormalization n)

The rescaled Hermite function is the √w-envelope of Hₙ(2√π·x). This is the identity that makes the general bridge produce TauCeti.twoPiHermiteFunction rather than some other normalization: Φₙ(x) = Hₙ(2√π·x)·e^{-πx²}/√cₙ.

theorem TauCeti.integral_twoPiHermiteFunction_mul_twoPiHermiteFunction (m n : ℕ) : ∫ (x : ℝ), twoPiHermiteFunction m x * twoPiHermiteFunction n x = if m = n then 1 else 0

Orthonormality of the rescaled family. The dilation u = √(2π)·x is unitary on L²(ℝ) by construction of the outer factor √(√(2π)), so the rescaled Hermite functions inherit the pointwise orthonormality of the ψₙ.

theorem TauCeti.integral_twoPiHermiteDilated_mul_twoPiHermiteDilated_mul_gaussianWeight (m n : ℕ) : ∫ (x : ℝ), Polynomial.eval x (twoPiHermiteDilated m) * Polynomial.eval x (twoPiHermiteDilated n) * Real.exp (-(2 * Real.pi * x ^ 2)) = if m = n then twoPiHermiteNormalization n else 0

The orthogonality relation of the Fourier-adapted system. ∫ Hₘ(2√π·x)Hₙ(2√π·x)e^{-2πx²} = δₘₙ·cₙ with cₙ = n!√π/√(2π); this is the input the bridge TauCeti.hilbertBasisOfOrthogonalSystem consumes.

L² packaging

theorem TauCeti.memLp_two_twoPiHermiteFunction (n : ℕ) : MeasureTheory.MemLp (twoPiHermiteFunction n) 2 MeasureTheory.volume

The rescaled Hermite functions lie in L²(ℝ): they are the image of the ψₙ under a dilation, which preserves square-integrability.

theorem TauCeti.memLp_two_algebraMap_twoPiHermiteFunction (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (twoPiHermiteFunction n x)) 2 MeasureTheory.volume

The scalar cast of a rescaled Hermite function lies in L²(ℝ; 𝕜).

noncomputable def TauCeti.twoPiHermiteFunctionLp (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)

The n-th rescaled Hermite function as a vector of L²(ℝ, volume; 𝕜).

Equations

• TauCeti.twoPiHermiteFunctionLp 𝕜 n = MeasureTheory.MemLp.toLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (TauCeti.twoPiHermiteFunction n x)) ⋯

theorem TauCeti.coeFn_twoPiHermiteFunctionLp (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↑↑(twoPiHermiteFunctionLp 𝕜 n) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => (algebraMap ℝ 𝕜) (twoPiHermiteFunction n x)

The Lp representative of TauCeti.twoPiHermiteFunctionLp is the scalar cast of the pointwise rescaled Hermite function.

noncomputable def TauCeti.twoPiHermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)

The rescaled Hermite functions are a Hilbert basis of L²(ℝ). This is the roadmap's Hermite basis in the normalization Mathlib's e^{-2πixξ} Fourier convention forces: the same bridge TauCeti.hilbertBasisOfOrthogonalSystem, run at the weight e^{-2πx²} and the polynomials Hₙ(2√π·x).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_twoPiHermiteHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : ⇑(twoPiHermiteHilbertBasis 𝕜) = twoPiHermiteFunctionLp 𝕜

The basis vectors are the rescaled Hermite functions. Without this the construction would only exhibit some Hilbert basis of L²(ℝ); here the √w-envelope of Hₙ(2√π·x)/√cₙ is identified with Φₙ.

theorem TauCeti.orthonormal_twoPiHermiteFunctionLp (𝕜 : Type u_1) [RCLike 𝕜] : Orthonormal 𝕜 (twoPiHermiteFunctionLp 𝕜)

The rescaled Hermite functions are orthonormal in L²(ℝ; 𝕜).

Diagonalization of the Fourier transform

noncomputable def TauCeti.twoPiHermiteSchwartzMap (n : ℕ) : SchwartzMap ℝ ℂ

The n-th rescaled Hermite function as a complex Schwartz function. It is built from TauCeti.hermiteSchwartzMap by the linear dilation x ↦ √(2π)·x and the inclusion ℝ → ℂ, both continuous linear operations on Schwartz space; this is what lets Mathlib's SchwartzMap.toLp_fourier_eq transfer the pointwise Fourier eigenrelation to L².

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.twoPiHermiteSchwartzMap_apply (n : ℕ) (x : ℝ) : (twoPiHermiteSchwartzMap n) x = ↑(twoPiHermiteFunction n x)

The underlying function of TauCeti.twoPiHermiteSchwartzMap is the rescaled Hermite function.

@[simp]

theorem TauCeti.coe_twoPiHermiteSchwartzMap (n : ℕ) : ⇑(twoPiHermiteSchwartzMap n) = fun (x : ℝ) => ↑(twoPiHermiteFunction n x)

The coercion of TauCeti.twoPiHermiteSchwartzMap is the complexified rescaled Hermite function.

theorem TauCeti.toLp_twoPiHermiteSchwartzMap (n : ℕ) : (twoPiHermiteSchwartzMap n).toLp 2 MeasureTheory.volume = twoPiHermiteFunctionLp ℂ n

The Schwartz function and the L² vector describe the same element of L²(ℝ; ℂ).

@[simp]

theorem TauCeti.fourier_twoPiHermiteSchwartzMap (n : ℕ) : FourierTransform.fourier (twoPiHermiteSchwartzMap n) = (-Complex.I) ^ n • twoPiHermiteSchwartzMap n

The Fourier eigenrelation in Schwartz space. This is the pointwise TauCeti.fourier_twoPiHermiteFunction read as an identity between Schwartz functions.

@[simp]

theorem TauCeti.fourier_twoPiHermiteFunctionLp (n : ℕ) : FourierTransform.fourier (twoPiHermiteFunctionLp ℂ n) = (-Complex.I) ^ n • twoPiHermiteFunctionLp ℂ n

The Fourier eigenrelation for the unitary Fourier transform of L²(ℝ; ℂ). The n-th rescaled Hermite function is an eigenvector of MeasureTheory.Lp.fourierTransformₗᵢ with eigenvalue (-i)ⁿ.

@[simp]

theorem TauCeti.fourierInv_twoPiHermiteFunctionLp (n : ℕ) : FourierTransformInv.fourierInv (twoPiHermiteFunctionLp ℂ n) = Complex.I ^ n • twoPiHermiteFunctionLp ℂ n

The inverse Fourier transform of L²(ℝ; ℂ) acts on the same eigenvectors with the conjugate eigenvalue iⁿ.

theorem TauCeti.hasSum_fourier_twoPiHermiteFunctionLp (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : HasSum (fun (n : ℕ) => ((-Complex.I) ^ n * ↑((twoPiHermiteHilbertBasis ℂ).repr f) n) • twoPiHermiteFunctionLp ℂ n) (FourierTransform.fourier f)

Diagonalization. The Fourier transform of an arbitrary f ∈ L²(ℝ; ℂ) is its expansion in the rescaled Hermite basis with the n-th coefficient multiplied by (-i)ⁿ.

@[simp]

theorem TauCeti.repr_fourier_twoPiHermiteHilbertBasis (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (n : ℕ) : ↑((twoPiHermiteHilbertBasis ℂ).repr (FourierTransform.fourier f)) n = (-Complex.I) ^ n * ↑((twoPiHermiteHilbertBasis ℂ).repr f) n

Diagonalization, coefficient form. Passing to the Fourier transform multiplies the n-th Hermite coefficient by (-i)ⁿ. This is the statement that the matrix of the Fourier transform in the rescaled Hermite basis is the diagonal matrix diag((-i)ⁿ).

@[simp]

theorem TauCeti.fourier_fourier_fourier_fourier (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : FourierTransform.fourier (FourierTransform.fourier (FourierTransform.fourier (FourierTransform.fourier f))) = f

The fourth iterate of the Fourier transform of L²(ℝ; ℂ) is the identity. Each eigenvalue (-i)ⁿ is a fourth root of unity, so the fourth iterate fixes every basis vector, hence all of L²(ℝ).