Nuclear Schauder Basis for S(ℝ, ℝ) — 1D Case

Assembles the proved Hermite function results into the three properties needed for a DyninMityaginSpace instance:

1. Expansion: φ f = ∑' n, cₙ(f) · φ(ψₙ) for all CLFs φ
2. Basis growth: ‖ψₙ‖_{k,l} ≤ C · (1+n)^s
3. Coefficient decay: |cₙ(f)| · (1+n)^k ≤ C · ‖f‖_{q₁,q₂}

All three are proved from theorems in HermiteFunctions.lean and SchwartzHermiteExpansion.lean. No axioms.

Hermite Coefficient as a Continuous Linear Map

hermiteCoeff1D is linear (proved) and bounded by a Schwartz seminorm (from the decay estimate at k=0), hence continuous.

noncomputable def hermiteCoeff1DCLM (n : ℕ) : SchwartzMap ℝ ℝ →L[ℝ] ℝ

The Hermite coefficient as a continuous linear map on Schwartz space.

Equations

• hermiteCoeff1DCLM n = { toFun := hermiteCoeff1D n, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem hermiteCoeff1DCLM_apply (n : ℕ) (f : SchwartzMap ℝ ℝ) : (hermiteCoeff1DCLM n) f = hermiteCoeff1D n f

Expansion Identity for Scalar CLFs

Specializing schwartz_hermite_expansion_1D to H = ℝ gives the expansion for arbitrary continuous linear functionals.

theorem schwartz_hermite_expansion_CLF (φ : SchwartzMap ℝ ℝ →L[ℝ] ℝ) (f : SchwartzMap ℝ ℝ) : φ f = ∑' (n : ℕ), hermiteCoeff1D n f * φ (schwartzHermiteBasis1D n)

The Hermite expansion recovers any continuous linear functional. For φ : S(ℝ) →L[ℝ] ℝ and f ∈ S(ℝ): φ(f) = ∑' n, cₙ(f) · φ(ψₙ)

Seminorm Bounds

The decay theorem bounds coefficients by a sup of finitely many seminorms. We show this sup is controlled by a single seminorm using:

• For the weight index k: ‖x‖^k' ≤ (1 + ‖x‖)^q.1 when k' ≤ q.1
• The one_add_le_sup_seminorm_apply lemma then bounds each pointwise value
• We apply seminorm_le_bound to lift to the seminorm level

Key fact: Mathlib's Schwartz seminorms use ‖x‖^k (NOT (1+‖x‖)^k), so they are NOT individually monotone in k. The bound goes through the (1+‖x‖) framework.

theorem hermiteCoeff1D_decay_single (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

Coefficient decay with a finset-sup seminorm bound. This is the natural form that follows directly from hermiteCoeff1D_decay.

Basis Growth (seminorm bound)

Repackage hermiteFunction_seminorm_bound with ℕ exponent.

theorem schwartzHermiteBasis1D_growth (k l : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (s : ℕ), ∀ (m : ℕ), (SchwartzMap.seminorm ℝ k l) (schwartzHermiteBasis1D m) ≤ C * (1 + ↑m) ^ s

Basis growth: Schwartz seminorms of Hermite functions grow polynomially. Compatible with DyninMityaginSpace.basis_growth.