Schwartz Hermite Expansion (1D)

Prove that for D = ℝ, F = ℝ, the Hermite expansion f = ∑' n, cₙ(f) · ψₙ converges in the Schwartz topology, implying the schwartz_hermite_expansion axiom.

Proof outline

1. Basis: ψₙ = hermiteFunction n, lifted to SchwartzMap ℝ ℝ
2. Coefficients: cₙ(f) = ∫ f(x) ψₙ(x) dx (a CLM on 𝓢)
3. Harmonic oscillator eigenvalue: -ψₙ'' + x²ψₙ = (2n+1)ψₙ (Follows from mul_x_hermiteFunction and deriv_hermiteFunction)
4. Integration by parts: ∫ Hf · ψₙ = (2n+1) ∫ f · ψₙ
5. Coefficient decay: |cₙ(f)| ≤ C·(2n+1)⁻ᵏ · p_q(f) for any k
6. Schwartz convergence: ∑ cₙ(f)ψₙ converges in each seminorm (Uses decay + hermiteFunction_seminorm_bound)
7. Identify limit: The Schwartz limit equals f (by L² uniqueness via hermiteFunction_complete)
8. Expansion identity: For any CLM T : 𝓢 →L[ℝ] H, continuity gives T(f) = ∑ cₙ(f) T(ψₙ)

Dependencies

Several lemmas in HermiteFunctions.lean are currently private and need to be exported:

• mul_x_hermiteFunction (raising/lowering identity)
• deriv_hermiteFunction (derivative identity)
• hermiteFunction_contDiff (smoothness)

Section 1: The 1D Schwartz Hermite Basis

noncomputable def schwartzHermiteBasis1D (n : ℕ) : SchwartzMap ℝ ℝ

The n-th Hermite function as a Schwartz map. Uses Classical.choose on hermiteFunction_schwartz n.

Equations

• schwartzHermiteBasis1D n = Classical.choose ⋯

theorem schwartzHermiteBasis1D_apply (n : ℕ) (x : ℝ) : (schwartzHermiteBasis1D n) x = hermiteFunction n x

The Schwartz map agrees with hermiteFunction n pointwise.

theorem schwartzHermiteBasis1D_coe (n : ℕ) : ⇑(schwartzHermiteBasis1D n) = hermiteFunction n

Coercion: the underlying function of the Schwartz map is hermiteFunction n.

Section 2: The 1D Hermite Coefficients

noncomputable def hermiteCoeff1D (n : ℕ) (f : SchwartzMap ℝ ℝ) : ℝ

The n-th Hermite coefficient of a Schwartz function f: cₙ(f) = ∫ f(x) ψₙ(x) dx.

Equations

• hermiteCoeff1D n f = ∫ (x : ℝ), f x * hermiteFunction n x

theorem hermiteCoeff1D_eq_integral (n : ℕ) (f : SchwartzMap ℝ ℝ) : hermiteCoeff1D n f = ∫ (x : ℝ), f x * hermiteFunction n x

The Hermite coefficient is the L² inner product with ψₙ.

theorem hermiteCoeff1D_linear (n : ℕ) : IsLinearMap ℝ (hermiteCoeff1D n)

Hermite coefficients are linear in f.

Section 3: Harmonic Oscillator Eigenvalue

The harmonic oscillator H = -d²/dx² + x² satisfies Hψₙ = (2n+1)ψₙ. This follows from combining:

• mul_x_hermiteFunction: x·ψₙ = √((n+1)/2)·ψ_{n+1} + √(n/2)·ψ_{n-1}
• deriv_hermiteFunction: ψₙ' = √(n/2)·ψ_{n-1} - √((n+1)/2)·ψ_{n+1}

Computing x²ψₙ (apply mul_x twice) and ψₙ'' (apply deriv twice), then subtracting gives -ψₙ'' + x²ψₙ = (2n+1)ψₙ.

NOTE: Currently blocked because mul_x_hermiteFunction and deriv_hermiteFunction are private in HermiteFunctions.lean.

theorem hermiteFunction_harmonic_oscillator_eigenvalue (n : ℕ) (x : ℝ) : -iteratedDeriv 2 (hermiteFunction n) x + x ^ 2 * hermiteFunction n x = (2 * ↑n + 1) * hermiteFunction n x

Section 4: Integration by Parts

For Schwartz functions f, integration by parts twice gives: ∫ f''·g = ∫ f·g'' (boundary terms vanish since f, g ∈ 𝓢 decay faster than any polynomial).

Combined with the eigenvalue equation, this yields: ∫ (-f'' + x²f) · ψₙ = (2n+1) ∫ f · ψₙ

i.e., cₙ(Hf) = (2n+1) · cₙ(f).

theorem schwartz_integration_by_parts_twice (f g : SchwartzMap ℝ ℝ) : ∫ (x : ℝ), iteratedDeriv 2 (⇑f) x * g x = ∫ (x : ℝ), f x * iteratedDeriv 2 (⇑g) x

Integration by parts: ∫ f'' g = ∫ f g'' for Schwartz functions.

theorem hermiteCoeff_harmonic_oscillator (n : ℕ) (f : SchwartzMap ℝ ℝ) : ∫ (x : ℝ), (-iteratedDeriv 2 (⇑f) x + x ^ 2 * f x) * hermiteFunction n x = (2 * ↑n + 1) * hermiteCoeff1D n f

The harmonic oscillator is symmetric on Schwartz space: ∫ Hf · ψₙ = (2n+1) ∫ f · ψₙ.

Section 5: Coefficient Decay

By iterating the harmonic oscillator identity k times: cₙ(f) = (2n+1)⁻ᵏ · cₙ(Hᵏf)

Combined with Cauchy-Schwarz: |cₙ(f)| ≤ (2n+1)⁻ᵏ · ‖Hᵏf‖_{L²}

And the Schwartz seminorm bound: ‖Hᵏf‖_{L²} ≤ C · p_q(f) for some q depending on k

This gives super-polynomial decay of Hermite coefficients.

theorem hermiteCoeff1D_decay (k : ℝ) : ∃ (C : ℝ) (q : ℕ × ℕ), 0 < C ∧ ∀ (f : SchwartzMap ℝ ℝ) (n : ℕ), |hermiteCoeff1D n f| * (1 + ↑n) ^ k ≤ C * ((Finset.Iic q).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm ℝ m.1 m.2) f

Section 6: Schwartz Convergence

The Hermite expansion converges absolutely in each Schwartz seminorm: ∑ₙ |cₙ(f)| · p_{k,l}(ψₙ) < ∞

This uses:

• hermiteCoeff1D_decay: |cₙ(f)| ≤ C(1+n)⁻ˢ · p_q(f) for any s
• hermiteFunction_seminorm_bound: p_{k,l}(ψₙ) ≤ C'(1+n)^σ
• Choose s > σ + 1: ∑ (1+n)^{σ-s} < ∞

theorem hermite_expansion_seminorm_summable (f : SchwartzMap ℝ ℝ) (k l : ℕ) : Summable fun (n : ℕ) => |hermiteCoeff1D n f| * (SchwartzMap.seminorm ℝ k l) (schwartzHermiteBasis1D n)

The Hermite expansion converges absolutely in each Schwartz seminorm.

theorem hermite_expansion_schwartz_seminorm_summable (f : SchwartzMap ℝ ℝ) (k l : ℕ) : Summable fun (n : ℕ) => (SchwartzMap.seminorm ℝ k l) (hermiteCoeff1D n f • schwartzHermiteBasis1D n)

The Hermite expansion ∑ cₙ(f) ψₙ converges in each Schwartz seminorm.

Section 7: Identify the Limit

The Schwartz series ∑ cₙ(f) ψₙ converges to some g ∈ 𝓢. Since g = f in L² (by hermiteFunction_complete and orthonormal expansion), and both are continuous, g = f everywhere.

theorem hermite_expansion_l2_convergence (f : SchwartzMap ℝ ℝ) : Filter.Tendsto (fun (N : ℕ) => ∫ (x : ℝ), (f x - ∑ n ∈ Finset.range N, hermiteCoeff1D n f * hermiteFunction n x) ^ 2) Filter.atTop (nhds 0)

Section 8: The 1D Expansion Theorem

Combining Schwartz convergence with limit identification: for any CLM T : 𝓢(ℝ,ℝ) →L[ℝ] H, ⟨w, T(f)⟩ = ∑' n, cₙ(f) · ⟨w, T(ψₙ)⟩

theorem schwartz_hermite_hasSum (f : SchwartzMap ℝ ℝ) : HasSum (fun (n : ℕ) => hermiteCoeff1D n f • schwartzHermiteBasis1D n) f

theorem schwartz_hermite_expansion_1D {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (T : SchwartzMap ℝ ℝ →L[ℝ] H) (f : SchwartzMap ℝ ℝ) (w : H) : inner ℝ w (T f) = ∑' (n : ℕ), hermiteCoeff1D n f * inner ℝ w (T (schwartzHermiteBasis1D n))