Nuclear Space Infrastructure for Schwartz Space

This file proves that Schwartz space is Hilbert-nuclear and separable, bridging between the gaussian-field library (Hermite-basis proofs) and the bochner library (Minlos theorem).

Proof chain

• SeparableSpace: directly from gaussian-field's Hermite analysis
• IsHilbertNuclear: gaussian-field's DyninMityaginSpace → NuclearSpace → bochner's IsNuclear → isHilbertNuclear_of_nuclear

References

• Trèves, "Topological Vector Spaces", Ch. 50-51
• Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. 3-4

WithSeminorms reindexing

A general reindexing lemma: if p generates the topology and e is an equivalence, then p ∘ e also generates the topology.

theorem WithSeminorms.equiv {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} {ι' : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (e : ι' ≃ ι) : WithSeminorms (p ∘ ⇑e)

Reindexing a seminorm family by an equivalence preserves WithSeminorms.

Bridge: gaussian-field NuclearSpace → bochner IsNuclear

gaussian-field's NuclearSpace (Pietsch characterization with ‖f n x‖) is equivalent to bochner's IsNuclear (same, with |f n x|), since for ℝ-valued CLFs, ‖y‖ = |y|.

theorem nuclearSpace_to_isNuclear {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [hN : GaussianField.NuclearSpace E] : IsNuclear E

Convert gaussian-field's NuclearSpace to bochner's IsNuclear.

Main instances for Schwartz space

instance schwartzIsHilbertNuclear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] : IsHilbertNuclear (SchwartzMap E ℝ)

Schwartz space is Hilbert-nuclear, proved via:

1. gaussian-field: DyninMityaginSpace (SchwartzMap D ℝ) (Hermite basis)
2. gaussian-field: DyninMityaginSpace → NuclearSpace (Pietsch characterization)
3. bridge: NuclearSpace → IsNuclear (norm = abs for ℝ)
4. bochner: isHilbertNuclear_of_nuclear (Pietsch → Hilbert-Schmidt embeddings)

instance schwartzSeparableSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] : TopologicalSpace.SeparableSpace (SchwartzMap E ℝ)

Schwartz space is separable, proved via Hermite analysis (gaussian-field).