# `NuclearSpace.lean` — Informal Summary

> **Source**: [`OSforGFF/Measure/NuclearSpace.lean`](../../OSforGFF/Measure/NuclearSpace.lean)
> **Generated**: 2026-03-10
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

This file proves that Schwartz space $\mathscr{S}(E, \mathbb{R})$ is Hilbert-nuclear and
separable, bridging between the `gaussian-field` library (Hermite-basis proofs, Dynin-Mityagin
characterization) and the `bochner` library (Minlos theorem, Pietsch factorization). The proof
chain converts `gaussian-field`'s `NuclearSpace` (using $\lVert \cdot \rVert$) to `bochner`'s
`IsNuclear` (using $\lvert \cdot \rvert$) via the identity $\lVert y \rVert = \lvert y \rvert$
for $\mathbb{R}$-valued CLFs, then applies `isHilbertNuclear_of_nuclear` with $\mathbb{N}$-reindexed
seminorms obtained via the Cantor pairing equivalence.

## Status
**Main result**: Fully proven (0 sorry, 0 axiom)

**Length**: 102 lines, 2 definition(s) + 2 theorem(s)/lemma(s)

---

## WithSeminorms reindexing

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

### [`WithSeminorms.equiv`](../../OSforGFF/Measure/NuclearSpace.lean#L42) — Theorem

**Statement**: If a seminorm family $p$ generates the topology via `WithSeminorms p`, and $e : \iota' \simeq \iota$ is an equivalence, then $p \circ e$ also generates the topology (i.e., `WithSeminorms (p \circ e)` holds).

**Proof uses**: `SeminormFamily.withSeminorms_iff_nhds_eq_iInf`, `Equiv.iInf_comp`

---

## Bridge: gaussian-field NuclearSpace to bochner IsNuclear

`gaussian-field`'s `NuclearSpace` (Pietsch characterization with $\lVert f_n(x) \rVert$) is
equivalent to `bochner`'s `IsNuclear` (same, with $\lvert f_n(x) \rvert$), since for
$\mathbb{R}$-valued CLFs, $\lVert y \rVert = \lvert y \rvert$.

### [`nuclearSpace_to_isNuclear`](../../OSforGFF/Measure/NuclearSpace.lean#L63) — Theorem

**Statement**: If $E$ carries a `GaussianField.NuclearSpace` instance, then $E$ satisfies `IsNuclear`. The proof rewrites the norm bound $\lVert f_n(x) \rVert \leq q(x)$ as $\lvert f_n(x) \rvert \leq q(x)$ using `Real.norm_eq_abs`.

**Proof uses**: `GaussianField.NuclearSpace.nuclear_dominance`, `Real.norm_eq_abs`

---

## Main instances for Schwartz space

### [`schwartz_isHilbertNuclear`](../../OSforGFF/Measure/NuclearSpace.lean#L82) — Definition (instance)

**Lean signature**
```lean
noncomputable instance schwartz_isHilbertNuclear {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] :
    IsHilbertNuclear (SchwartzMap E ℝ)
```

**Informal**: The Schwartz space $\mathscr{S}(E, \mathbb{R})$ is Hilbert-nuclear. The proof proceeds in four steps: (1) obtain `NuclearSpace` from `DyninMityaginSpace` via `gaussian-field`, (2) convert to `IsNuclear` via `nuclearSpace_to_isNuclear`, (3) reindex the two-parameter Schwartz seminorm family to $\mathbb{N}$ using the Cantor pairing equivalence and `WithSeminorms.equiv`, (4) apply `isHilbertNuclear_of_nuclear`.

**Proof uses**: `GaussianField.DyninMityaginSpace.toNuclearSpace`, `nuclearSpace_to_isNuclear`, `WithSeminorms.equiv`, `Nat.pairEquiv`, `schwartz_withSeminorms`, `isHilbertNuclear_of_nuclear`

---

### [`schwartz_separableSpace`](../../OSforGFF/Measure/NuclearSpace.lean#L99) — Definition (instance)

**Lean signature**
```lean
noncomputable instance schwartz_separableSpace {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] :
    SeparableSpace (SchwartzMap E ℝ)
```

**Informal**: The Schwartz space $\mathscr{S}(E, \mathbb{R})$ is separable, proved directly from the Hermite analysis in `gaussian-field`.

**Proof uses**: `GaussianField.schwartz_separableSpace`

---

*This file has **2** definitions and **2** theorems/lemmas (0 with sorry).*