# `WhiteNoise.lean` — Informal Summary

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

## Overview

This file demonstrates an application of the Minlos theorem to construct **white noise** as a probability measure on the dual of Schwartz space $S'(\mathbb{R})$. The white noise characteristic functional $\Phi(f) = \exp(-\tfrac{1}{2} \lVert f \rVert_{L^2}^2)$ is shown to determine a unique probability measure on $\mathrm{WeakDual}\;\mathbb{R}\;(\mathrm{SchwartzMap}\;\mathbb{R}\;\mathbb{R})$. Four domain-specific axioms encode standard facts about Schwartz space (separability, Hilbert-nuclearity, L2 seminorm continuity, positive-definiteness of the Gaussian kernel) that are provable from Hermite basis theory and the gaussian-field project but not yet formalized in Mathlib. A bridge theorem establishes that any probability measure with the same CF (e.g., one constructed by the gaussian-field project) must equal the Minlos-constructed measure.

## Status

**Main result**: `white_noise_measure_exists` — existence and uniqueness of white noise measure on $S'(\mathbb{R})$ via Minlos' theorem.
**Length**: 133 lines, 1 definition(s) + 3 theorem(s)/lemma(s) + 4 axiom(s)

---

### `schwartz_separableSpace` (axiom, L64)

[`schwartz_separableSpace`](../../Test/WhiteNoise.lean#L64)

**Statement**: Schwartz space $\mathcal{S}(\mathbb{R})$ is separable.

```
axiom schwartz_separableSpace : SeparableSpace (SchwartzMap ℝ ℝ)
```

The Hermite basis provides a countable dense set.

---

### `schwartz_isHilbertNuclear` (axiom, L72)

[`schwartz_isHilbertNuclear`](../../Test/WhiteNoise.lean#L72)

**Statement**: Schwartz space $\mathcal{S}(\mathbb{R})$ is nuclear in the Hilbertian sense (`IsHilbertNuclear`).

```
axiom schwartz_isHilbertNuclear : IsHilbertNuclear (SchwartzMap ℝ ℝ)
```

Derivable from the gaussian-field project's proof that $\mathcal{S}(\mathbb{R})$ is a Dynin--Mityagin space (hence Pietsch nuclear), composed with `isHilbertNuclear_of_nuclear` from [`PietschBridge.lean`](../../Minlos/PietschBridge.lean). The Hermite--Sobolev norms $\lVert f \rVert_k^2 = \sum_n (1+n)^{2k} \lvert \langle f, h_n \rangle \rvert^2$ are Hilbertian with HS consecutive inclusions since $\sum (1+n)^{-2} < \infty$.

---

### `schwartzMap_l2Norm_continuous` (axiom, L77)

[`schwartzMap_l2Norm_continuous`](../../Test/WhiteNoise.lean#L77)

**Statement**: The map $f \mapsto \int_{\mathbb{R}} (f(x))^2\,dx$ is continuous on the Schwartz topology.

```
axiom schwartzMap_l2Norm_continuous :
    Continuous (fun f : SchwartzMap ℝ ℝ => ∫ x : ℝ, (f x) ^ 2)
```

Follows from rapid decay: $\int f^2 \leq (\int (1+x^2)^{-1}\,dx) \cdot \sup_x (1+x^2)\lvert f(x)\rvert^2$.

---

### `whiteNoiseCF` (definition, L89)

[`whiteNoiseCF`](../../Test/WhiteNoise.lean#L89)

```lean
def whiteNoiseCF : SchwartzMap ℝ ℝ → ℂ :=
  fun f => exp (-(1 / 2 : ℂ) * ↑(∫ x : ℝ, (f x) ^ 2))
```

The white noise characteristic functional $\Phi(f) = \exp\!\bigl(-\tfrac{1}{2} \int_{\mathbb{R}} f(x)^2\,dx\bigr)$. When the gaussian-field project's `GaussianField.measure` is applied with $T = \mathrm{inclusion}\;\mathcal{S}(\mathbb{R}) \hookrightarrow L^2(\mathbb{R})$, the resulting CF $\exp(-\tfrac{1}{2}\langle Tf, Tf \rangle_{L^2})$ is definitionally equal.

---

### `whiteNoiseCF_normalized` (theorem, L93)

[`whiteNoiseCF_normalized`](../../Test/WhiteNoise.lean#L93)

**Statement**: $\Phi(0) = 1$.

**Proof**: Direct computation using `integral_zero`.

**Dependencies**: `whiteNoiseCF`.

---

### `whiteNoiseCF_continuous` (theorem, L98)

[`whiteNoiseCF_continuous`](../../Test/WhiteNoise.lean#L98)

**Statement**: $\Phi$ is continuous on Schwartz space.

**Proof**: Composition of `continuous_exp`, `continuous_const.mul`, `continuous_ofReal`, and the axiom `schwartzMap_l2Norm_continuous`.

**Dependencies**: `whiteNoiseCF`, `schwartzMap_l2Norm_continuous`.

---

### `whiteNoiseCF_pd` (axiom, L108)

[`whiteNoiseCF_pd`](../../Test/WhiteNoise.lean#L108)

**Statement**: $\Phi(f) = \exp(-\tfrac{1}{2}\lVert f \rVert_{L^2}^2)$ is positive definite.

```
axiom whiteNoiseCF_pd : IsPositiveDefinite whiteNoiseCF
```

Derivable from gaussian-field's `GaussianField.charFun` (the CF of any probability measure is PD), or directly from Schoenberg's theorem (the Gaussian RBF $e^{-\frac{1}{2}\lVert x \rVert^2}$ is PD on any inner product space) pulled back via [`IsPositiveDefinite`](../../Bochner/PositiveDefinite.lean).

---

### `white_noise_measure_exists` (theorem, L115)

[`white_noise_measure_exists`](../../Test/WhiteNoise.lean#L115)

**Statement**: There exists a unique probability measure $\mu$ on $S'(\mathbb{R}) = \mathrm{WeakDual}\;\mathbb{R}\;(\mathrm{SchwartzMap}\;\mathbb{R}\;\mathbb{R})$ such that for all $f \in \mathcal{S}(\mathbb{R})$,
$$\Phi(f) = \int_{S'(\mathbb{R})} e^{i\,\omega(f)}\,d\mu(\omega).$$

**Proof**: Direct application of [`minlos_theorem`](../../Minlos/Main.lean) to `whiteNoiseCF` with its continuity, positive-definiteness, and normalization.

**Dependencies**: [`minlos_theorem`](../../Minlos/Main.lean), `whiteNoiseCF`, `whiteNoiseCF_continuous`, `whiteNoiseCF_pd`, `whiteNoiseCF_normalized`, `schwartz_separableSpace`, `schwartz_isHilbertNuclear`.

---

### `white_noise_unique` (theorem, L126)

[`white_noise_unique`](../../Test/WhiteNoise.lean#L126)

**Statement**: If $\mu_1$ and $\mu_2$ are any two probability measures on $S'(\mathbb{R})$ whose characteristic functionals both equal $\Phi(f) = \exp(-\tfrac{1}{2}\lVert f \rVert_{L^2}^2)$, then $\mu_1 = \mu_2$.

This is the **bridge theorem** with the gaussian-field project: any measure constructed by any method with the white noise CF must equal the Minlos-constructed measure.

**Proof**: Direct application of [`minlos_uniqueness`](../../Minlos/Main.lean).

**Dependencies**: [`minlos_uniqueness`](../../Minlos/Main.lean), `whiteNoiseCF_continuous`, `whiteNoiseCF_pd`, `whiteNoiseCF_normalized`.

---

*This file has **1** definition and **3** theorems/lemmas (0 with sorry), plus **4** axioms.*