# Nuclear Spaces and Gaussian Measure Construction

## The Problem: Fields Are Not Functions

In quantum mechanics, one writes the wave function $\psi(x)$ and evaluates it at
a point. In quantum field theory, the analogous object $\Phi(x)$ is not a
function --- it is a distribution. This is already visible in the free field:
the Gaussian free field (GFF) on $\mathbb{R}^d$ for $d \geq 2$ has sample paths
that are too rough to evaluate at a point. More precisely, the covariance

$$\langle \Phi(x) \Phi(y) \rangle = G(x, y) = \frac{1}{(2\pi)^d} \int \frac{e^{ik \cdot (x - y)}}{|k|^2 + m^2}\, dk$$

diverges logarithmically as $x \to y$ in $d = 2$, and with a power-law
singularity in higher dimensions. The "field at a point" does not exist as a
random variable.

The resolution is to **smear**: instead of $\Phi(x)$, one works with

$$\Phi(f) = \int \Phi(x)\, f(x)\, dx$$

for test functions $f$ in Schwartz space $\mathscr{S}(\mathbb{R}^d)$. The
smeared field $\Phi(f)$ is a well-defined Gaussian random variable with variance

$$\operatorname{Var}[\Phi(f)] = \langle f, (-\Delta + m^2)^{-1} f \rangle_{L^2} < \infty.$$

This is finite because the test function $f$ kills the ultraviolet divergence.
A quantum field is therefore not a random function $\Phi : \mathbb{R}^d \to \mathbb{R}$,
but a random linear functional $\omega : \mathscr{S}(\mathbb{R}^d) \to \mathbb{R}$ ---
a tempered distribution. The probability measure describing the field lives on
the space of tempered distributions $\mathscr{S}'(\mathbb{R}^d)$.

## The Gel'fand Triple

The natural framework is a **Gel'fand triple** (also called a rigged Hilbert space):

$$\mathscr{S} \hookrightarrow L^2 \hookrightarrow \mathscr{S}'.$$

- **$\mathscr{S}$** (Schwartz space): the space of smooth rapidly decreasing test
  functions. This is where we probe the field. It is a nuclear Frechet space,
  topologized by the seminorms $p_{k,n}(f) = \sup_x (1 + |x|)^k |\partial^\alpha f(x)|$.
- **$L^2$**: the Hilbert space, where the covariance operator $(-\Delta + m^2)^{-1}$
  naturally acts. This is the "middle" space connecting test functions to
  distributions.
- **$\mathscr{S}'$**: tempered distributions, the continuous dual of $\mathscr{S}$.
  This is the configuration space --- the space where the measure lives.

In the formalization, the configuration space is:

```lean
abbrev Configuration (E : Type*)
    [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] [IsTopologicalAddGroup E]
    [ContinuousSMul ℝ E] := WeakDual ℝ E
```

An element $\omega$ of `Configuration E` is a continuous linear functional
$\omega : E \to \mathbb{R}$. Evaluation $\omega(f)$ is the smeared field value.
The measurable structure is the **cylindrical $\sigma$-algebra**, generated by
the evaluation maps $\omega \mapsto \omega(f)$ for all $f \in E$. This is the
coarsest $\sigma$-algebra making all smeared fields measurable:

```lean
instance instMeasurableSpaceConfiguration :
    MeasurableSpace (Configuration E) :=
  MeasurableSpace.comap (fun ω f => ω f) MeasurableSpace.pi
```

## Nuclear Spaces and Why They Matter

The central question is: **how do you construct a probability measure on an
infinite-dimensional space?**

In finite dimensions, you can specify a measure by its density, or by its
characteristic function (Fourier transform). The classical Bochner theorem
says that a continuous positive-definite function $\chi : \mathbb{R}^n \to \mathbb{C}$
with $\chi(0) = 1$ is the characteristic function of a unique probability measure.

In infinite dimensions, this fails catastrophically. There is no Lebesgue
measure on an infinite-dimensional Hilbert space. One cannot simply write down
a density. Worse, the naive extension of Bochner's theorem fails: continuous
positive-definite functionals on a Hilbert space need not correspond to measures.
The standard example is $\chi(f) = e^{-\|f\|^2/2}$ on $L^2$ --- this looks like
it should be the characteristic functional of a Gaussian, but no such measure
exists on $L^2$.

The **Bochner--Minlos theorem** resolves this by restricting the domain:

> **Theorem** (Bochner--Minlos). *Let $E$ be a nuclear space. A functional
> $\chi : E \to \mathbb{C}$ is the characteristic functional of a probability
> measure on $E'$ (the continuous dual) if and only if $\chi$ is continuous,
> positive-definite, and $\chi(0) = 1$.*

The key word is **nuclear**. Nuclearity is the infinite-dimensional property
that makes the construction work. Intuitively, a nuclear space is "almost
finite-dimensional" in the sense that every continuous linear map from it to a
Hilbert space can be approximated by finite-rank maps with summable singular
values.

More precisely, a locally convex space $E$ is nuclear if for every continuous
seminorm $p$, there exists a stronger continuous seminorm $q$ such that the
canonical map from the $q$-completion to the $p$-completion is **trace class**
(has summable singular values). This is much stronger than compactness --- it
says the embedding is not just compact but has summable eigenvalues.

For the P($\Phi$)$_2$ construction, nuclearity is essential at several points:

1. **Measure existence**: The Gaussian free field measure is constructed via
   Bochner--Minlos, using the characteristic functional
   $\chi(f) = \exp(-\frac{1}{2}\langle Tf, Tf \rangle_H)$.
2. **Tightness**: Compact sets in $\mathscr{S}'$ are characterized by
   "coordinate boxes" with polynomial growth bounds. The nuclear structure
   gives quantitative control over these boxes, enabling the Prokhorov
   compactness argument for the continuum limit.
3. **Uniqueness**: The cylindrical $\sigma$-algebra on $\mathscr{S}'$ is
   generated by countably many evaluations (at the basis elements), allowing
   Dynkin's $\pi$-$\lambda$ theorem to extend equality from cylinder sets to
   the full $\sigma$-algebra.

Schwartz space $\mathscr{S}(\mathbb{R}^d)$ is nuclear. This is ultimately why
Schwartz space is the "right" test function space for quantum field theory ---
not merely because its elements are smooth and rapidly decreasing, but because
its nuclearity is what makes the measure theory work.

## The Dynin--Mityagin Characterization

The formalization does not work with nuclearity in its full generality. Instead,
it uses a concrete characterization due to Dynin and Mityagin: a nuclear Frechet
space with a countable Schauder basis is isomorphic to a **Kothe sequence space**
with rapidly decaying weights.

This is captured by the `DyninMityaginSpace` typeclass:

```lean
class DyninMityaginSpace (E : Type*)
    [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] [IsTopologicalAddGroup E]
    [ContinuousSMul ℝ E] extends T1Space E where
  ι : Type
  p : ι → Seminorm ℝ E
  h_with : WithSeminorms p
  h_countable : Countable ι
  h_completeSpace : @CompleteSpace E ...
  basis : ℕ → E
  coeff : ℕ → (E →L[ℝ] ℝ)
  expansion : ∀ (φ : E →L[ℝ] ℝ) (f : E),
    φ f = ∑' m, (coeff m f) * φ (basis m)
  basis_growth :
    ∀ (i : ι), ∃ C > 0, ∃ (s : ℕ),
    ∀ m, p i (basis m) ≤ C * (1 + (m : ℝ)) ^ s
  coeff_decay :
    ∀ (k : ℕ), ∃ C > 0, ∃ (s : Finset ι),
    ∀ f m, |coeff m f| * (1 + (m : ℝ)) ^ k ≤ C * (s.sup p) f
```

The axioms encode two crucial properties:

- **Basis growth** (`basis_growth`): the basis elements $\psi_m$ grow at most
  polynomially in every seminorm: $p_i(\psi_m) \leq C(1 + m)^s$. This says
  the basis elements, while not bounded, grow controllably.
- **Coefficient decay** (`coeff_decay`): the expansion coefficients $c_m(f)$
  decay faster than any polynomial: $|c_m(f)| \cdot (1 + m)^k \leq C \cdot q(f)$
  for some continuous seminorm $q$, for any power $k$. This is the "rapid decay"
  condition that encodes nuclearity.

The interplay between polynomial growth and rapid decay is where summability
comes from. If the $m$-th coefficient decays like $(1+m)^{-k}$ for any $k$,
and the $m$-th basis element grows like $(1+m)^s$, then their product decays
like $(1+m)^{s-k}$, which is summable for $k > s + 1$. This is the mechanism
behind the nuclear factorization.

For Schwartz space, the Hermite functions $\{h_\alpha\}$ provide the Schauder
basis. In one dimension, $h_n(x) = H_n(x) e^{-x^2/2}$ where $H_n$ is the
$n$-th Hermite polynomial. These are eigenfunctions of the harmonic oscillator,
and their seminorm growth is polynomial in $n$. The instance is proved in
the `gaussian-field` library:

```lean
noncomputable instance schwartz_dyninMityaginSpace [Nontrivial D] :
    DyninMityaginSpace (SchwartzMap D ℝ) :=
  DyninMityaginSpace.ofRapidDecayEquiv
    (fun (kl : ℕ × ℕ) => SchwartzMap.seminorm ℝ kl.1 kl.2)
    (schwartz_withSeminorms ℝ D ℝ)
    (schwartzRapidDecayEquiv D)
```

The proof constructs the topological isomorphism
$\mathscr{S}(\mathbb{R}^d) \cong \ell_{\text{rapid}}$ (the space of rapidly
decaying sequences) via multi-dimensional Hermite analysis.

Every $\omega \in \mathscr{S}'$ is determined by its values on the basis:
$\omega \mapsto (\omega(\psi_m))_{m \in \mathbb{N}}$. Compact sets in
$\mathscr{S}'$ are precisely "coordinate boxes" of the form
$\{\omega : |\omega(\psi_m)| \leq R_m\}$ where $R_m$ grows at most polynomially.
This characterization is essential for proving tightness of measure families.

## Gaussian Measure Construction

With the nuclear framework in place, the Gaussian measure construction proceeds
as follows. The input is a continuous linear map $T : E \to H$ from a nuclear
Frechet space to a separable Hilbert space. The output is a probability measure
$\mu$ on $\mathscr{S}'$ (i.e., on `Configuration E`) with covariance

$$C(f, g) = \langle T(f), T(g) \rangle_H.$$

The construction has four steps:

### Step 1: Nuclear Factorization

From the Dynin--Mityagin structure, extract an adapted orthonormal basis
$\{e_n\}$ of $H$, an intermediate Hilbert space $K$ (concretely, $\ell^2$), a
CLM $j : E \to K$, and vectors $v_n \in K$ satisfying:

- $\sum_n \|v_n\| < \infty$ (this is the nuclearity condition),
- $\langle e_n, T(f) \rangle_H = \langle v_n, j(f) \rangle_K$ for all $f \in E$
  and $n \in \mathbb{N}$.

The summability $\sum \|v_n\| < \infty$ is the key property that would fail
for non-nuclear spaces.

### Step 2: Noise Measure

Construct the product measure $\mu_{\text{noise}} = \bigotimes_n N(0,1)$ on
$\mathbb{R}^{\mathbb{N}}$ --- a countable product of standard Gaussians. This
is the source of randomness.

### Step 3: Series Limit

For a.e. noise realization $\xi = (\xi_0, \xi_1, \ldots)$, define

$$\omega(f) = \sum_{n=0}^{\infty} \xi_n \langle e_n, T(f) \rangle_H = \Big\langle \sum_n \xi_n v_n,\, j(f) \Big\rangle_K.$$

The series converges a.s. because $\sum \|v_n\| < \infty$ and $\xi_n$ are iid
standard Gaussians (so $\|\sum \xi_n v_n\|$ is controlled by the summability of
$\|v_n\|$). The limit $\omega$ is a continuous linear functional on $E$, hence
an element of `Configuration E`.

### Step 4: Pushforward

The Gaussian measure is the pushforward:

$$\mu = (\text{seriesLimit})_* \mu_{\text{noise}}.$$

In the formalization:

```lean
noncomputable def measure (T : E →L[ℝ] H) :
    @Measure (Configuration E) instMeasurableSpaceConfiguration :=
  if hfin : FiniteDimensional ℝ H then
    Measure.map (seriesLimit ((hilbertEmbedding hfin).comp T)
      ell2_not_finiteDimensional) noiseMeasure
  else
    Measure.map (seriesLimit T hfin) noiseMeasure
```

(The finite-dimensional case embeds $H$ isometrically into $\ell^2$ first, to
use the infinite-dimensional factorization machinery uniformly.)

### The Characteristic Functional

The central identity is:

$$\int e^{i\omega(f)}\, d\mu(\omega) = \exp\!\Big(-\tfrac{1}{2}\langle T(f), T(f) \rangle_H\Big).$$

This is the statement that $\mu$ is Gaussian with the correct covariance. The
proof (`charFun` in `Construction.lean`) reduces to a product of 1D Gaussian
characteristic functions via the independence of the $\xi_n$:

$$\int \prod_n e^{i \xi_n \langle e_n, Tf \rangle}\, d\mu_{\text{noise}} = \prod_n e^{-\frac{1}{2} |\langle e_n, Tf \rangle|^2} = e^{-\frac{1}{2} \|Tf\|^2}$$

where the last step is Parseval's identity.

## Identifying Gaussian Limits

In the P($\Phi$)$_2$ construction, one works with lattice approximations: the
lattice Gaussian free field on a grid of spacing $a$, embedded into the
continuum space $\mathscr{S}'(\mathbb{R}^d)$. As $a \to 0$, one extracts a
subsequential weak limit via Prokhorov's theorem (using tightness from
hypercontractivity bounds). But how does one identify this limit?

There are two key results:

### Uniqueness from Covariance

**Theorem** (`gaussian_measure_unique_of_covariance`). *If $\mu_1$ and $\mu_2$
are centered Gaussian probability measures on $\mathscr{S}'$ with the same
covariance, then $\mu_1 = \mu_2$.*

The proof proceeds in stages:

1. **Same covariance implies same MGF**: For each test function $f$,
   $\int e^{t\,\omega(f)}\, d\mu_1 = e^{t^2 \sigma^2/2} = \int e^{t\,\omega(f)}\, d\mu_2$
   where $\sigma^2 = \int (\omega f)^2\, d\mu$.
2. **Same MGF implies same 1D marginals**: By analytic continuation
   (the MGF extends to a complex neighborhood, where it equals the
   characteristic function) and the uniqueness theorem for characteristic
   functions, $(\text{ev}_f)_* \mu_1 = (\text{ev}_f)_* \mu_2$ for every $f$.
3. **Same 1D marginals for all $f$ implies same finite-dimensional marginals**:
   By the Cramer--Wold theorem, knowing all 1D projections determines the
   joint distribution.
4. **Finite-dimensional marginals determine the measure**: By Dynkin's
   $\pi$-$\lambda$ theorem, agreement on cylinder sets (which form a
   $\pi$-system) extends to the full cylindrical $\sigma$-algebra.

This is fully proved in `MeasureUniqueness.lean` (0 axioms, 0 sorries).

### Gaussianity

The construction produces a measure that is Gaussian in the Mathlib sense:

```lean
instance measure_isGaussian (T : E →L[ℝ] H) :
    ProbabilityTheory.IsGaussian (measure T) where
  map_eq_gaussianReal L := ...
```

This requires showing that every continuous linear functional on
`WeakDual ℝ E` is evaluation at some $f \in E$ --- the standard fact that the
continuous dual of the weak-$*$ topology is the original space. This is proved
in `IsGaussian.lean` as `weakDual_clm_eq_eval`, via a finite-dimensionality
argument using the initial topology characterization.

## Formalization Status

The following table summarizes what is proved versus axiomatized in the
`gaussian-field` library and its use in the P($\Phi$)$_2$ project.

| Component | Status | Location |
|-----------|--------|----------|
| `DyninMityaginSpace` typeclass | Proved | `Nuclear/DyninMityagin.lean` |
| Schwartz space instance | Proved | `SchwartzNuclear/HermiteNuclear.lean` |
| Nuclear factorization | Proved | `TargetFactorization.lean` |
| Gaussian measure construction | Proved | `Construction.lean` |
| Characteristic functional | Proved | `Construction.lean` (`charFun`) |
| Probability measure instance | Proved | `Construction.lean` (`measure_isProbability`) |
| `IsGaussian` instance | Proved | `IsGaussian.lean` (`measure_isGaussian`) |
| Weak dual CLM = evaluation | Proved | `IsGaussian.lean` (`weakDual_clm_eq_eval`) |
| Uniqueness from covariance | Proved | `MeasureUniqueness.lean` |
| Gaussianity of weak limits | **Axiom** | `GaussianLimit.lean` (`gaussianLimit_isGaussian`) |

The remaining axiom, `gaussianLimit_isGaussian`, states that weak limits of
centered Gaussian measures (with converging covariance) are again Gaussian.
This is a consequence of the Bochner--Minlos theorem: if the characteristic
functionals $\chi_n(f) = \exp(-\frac{1}{2}\sigma_n^2(f))$ converge pointwise
to $\chi(f) = \exp(-\frac{1}{2}\sigma^2(f))$, then $\chi$ is again continuous
and positive-definite, hence the characteristic functional of a Gaussian
measure. The formalization of this continuity argument (showing that pointwise
convergence of variances implies continuity of the limiting characteristic
functional in the nuclear topology) is the remaining gap.

## References

- I.M. Gel'fand and N.Ya. Vilenkin, *Generalized Functions*, Vol. 4:
  *Applications of Harmonic Analysis*, Academic Press, 1964. Chapters 3--4
  develop the theory of measures on nuclear spaces and the Bochner--Minlos
  theorem.
- X. Fernique, "Regularite des trajectoires des fonctions aleatoires
  gaussiennes," *Ecole d'Ete de Probabilites de Saint-Flour IV*, Lecture Notes
  in Math. **480**, Springer, 1975, pp. 1--96. Develops Gaussian measures
  on locally convex spaces with applications to regularity.
- B. Simon, *The P($\phi$)$_2$ Euclidean (Quantum) Field Theory*, Princeton
  University Press, 1974, Chapter I. Constructs the free Euclidean field as
  a Gaussian measure on $\mathscr{S}'(\mathbb{R}^2)$.
- J. Glimm and A. Jaffe, *Quantum Physics: A Functional Integral Point of
  View*, 2nd ed., Springer, 1987, Section 6.2 (Gaussian measures) and
  Section 19.1 (the free field).
- A. Dynin and B. Mityagin, "Criterion for nuclearity in terms of
  approximative dimension," *Bull. Acad. Polon. Sci.* **8** (1960), 535--540.