# `Construction.lean` — Informal Summary

> **Source**: [`GaussianField/Construction.lean`](../../GaussianField/Construction.lean)
> **Generated**: 2026-03-03 11:30
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Constructs a centered Gaussian probability measure $\mu$ on the weak dual $E'$ of a nuclear Frechet space $E$, given a continuous linear map $T : E \to H$ into a separable Hilbert space. The covariance is $C(f,g) = \langle T(f), T(g) \rangle_H$. The construction uses a nuclear SVD to produce iid $N(0,1)$ noise on $\mathbb{R}^\mathbb{N}$, then pushes forward through a series-limit map. The main theorem proves the characteristic functional identity $\mathbb{E}[e^{i\langle \omega, f \rangle}] = e^{-\frac{1}{2}\lVert T(f) \rVert^2}$.

## Status

**Main result**: Fully proven

None --- file is sorry-free.

**Length**: 715 lines, 14 definition(s) + 18 theorem(s)/lemma(s)

---

## Configuration Space

### `Configuration` --- Definition

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

**Informal**: The configuration space $E' = \mathrm{WeakDual}(\mathbb{R}, E)$ of continuous linear functionals on $E$.

---

### `instMeasurableSpaceConfiguration` --- Definition

**Lean signature**
```lean
instance instMeasurableSpaceConfiguration :
    MeasurableSpace (Configuration E)
```

**Informal**: The cylindrical $\sigma$-algebra on $\mathrm{Configuration}(E)$, generated by evaluation maps $\omega \mapsto \omega(f)$.

---

### [`configuration_measurable_of_eval_measurable`](../../GaussianField/Construction.lean#L74) --- Theorem

**Statement**: A function $g : X \to \mathrm{Configuration}(E)$ is measurable (w.r.t. the cylindrical $\sigma$-algebra) if and only if all evaluations $x \mapsto g(x)(\varphi)$ are measurable.

**Proof uses**: `measurable_iff_comap_le`, `MeasurableSpace.comap_comp`, `measurable_pi_lambda`

---

### [`configuration_eval_measurable`](../../GaussianField/Construction.lean#L85) --- Theorem

**Statement**: Each evaluation map $\omega \mapsto \omega(\varphi)$ is measurable w.r.t. the cylindrical $\sigma$-algebra.

**Proof uses**: `measurable_pi_apply`

---

### `covariance` --- Definition

**Lean signature**
```lean
def covariance (T : E →L[ℝ] H) (f g : E) : ℝ
```

**Informal**: The covariance bilinear form $C(f,g) = \langle T(f), T(g) \rangle_H$.

---

## Factorization Extraction

### `adaptedBasis` --- Definition (private)

**Lean signature**
```lean
private noncomputable def adaptedBasis (T : E →L[ℝ] H)
    (h_inf : ¬ FiniteDimensional ℝ H) : HilbertBasis ℕ ℝ H
```

**Informal**: The adapted Hilbert basis for $H$ extracted from the nuclear factorization of $T$, used to establish Parseval's identity.

---

### `coeff` --- Definition (private)

**Lean signature**
```lean
private noncomputable def coeff (T : E →L[ℝ] H)
    (h_inf : ¬ FiniteDimensional ℝ H) (n : ℕ) (f : E) : ℝ
```

**Informal**: The $n$-th Fourier coefficient of $T(f)$ in the adapted ONB: $c_n(f) = \langle e_n, T(f) \rangle_H$.

---

### [`coeff_sq_summable`](../../GaussianField/Construction.lean#L179) --- Lemma (private)

**Statement**: For each $f$, the sequence $(c_n(f))^2$ is summable (by Parseval's identity).

**Proof uses**: `Memℓp.summable`, `HilbertBasis.repr_apply_apply`

---

### [`coeff_parseval`](../../GaussianField/Construction.lean#L197) --- Lemma (private)

**Statement**: Parseval's identity: $\sum_n c_n(f)^2 = \lVert T(f) \rVert^2$.

**Proof uses**: `HilbertBasis.repr.norm_map`, `lp.norm_rpow_eq_tsum`, `HilbertBasis.repr_apply_apply`

---

## Noise Measure

### `NoiseSpace` --- Definition

**Lean signature**
```lean
abbrev NoiseSpace := ℕ → ℝ
```

**Informal**: The space of noise sequences $\xi : \mathbb{N} \to \mathbb{R}$.

---

### `noiseMeasure` --- Definition (private)

**Lean signature**
```lean
private noncomputable def noiseMeasure : Measure NoiseSpace
```

**Informal**: The infinite product measure $\mu_{\mathrm{noise}} = \bigotimes_n N(0,1)$ of iid standard Gaussians.

---

## Series Limit Map

### `seriesLimit` --- Definition (private)

**Lean signature**
```lean
private noncomputable def seriesLimit
    (T : E →L[ℝ] H) (h_inf : ¬ FiniteDimensional ℝ H)
    (ξ : NoiseSpace) : Configuration E
```

**Informal**: For a noise sequence $\xi$, the series limit $\omega(f) = \sum_n \xi_n c_n(f)$ as an element of $E'$. Continuity follows from the CLM factorization through the intermediate space $K$.

---

### [`hilbert_gaussian_series_converges`](../../GaussianField/Construction.lean#L327) --- Theorem (private)

**Statement**: If $\sum_n \lVert v_n \rVert < \infty$ and $\xi_n \sim \text{iid } N(0,1)$, then $\sum_n \xi_n v_n$ converges almost surely in $K$. Proved via Tonelli: $\mathbb{E}[\sum \lVert \xi_n v_n \rVert] = C \cdot \sum \lVert v_n \rVert < \infty$.

**Proof uses**: `IsGaussian.integrable_dual`, `measurePreserving_eval_infinitePi`, `lintegral_tsum`, `ae_lt_top`

---

### [`aemeasurable_seriesLimit`](../../GaussianField/Construction.lean#L399) --- Theorem (private)

**Statement**: The series limit map is AE-measurable w.r.t. the noise measure.

**Proof uses**: [`configuration_measurable_of_eval_measurable`](../../GaussianField/Construction.lean#L74), [`isGoodNoise_ae`](../../GaussianField/Construction.lean#L375), [`limUnder_partialSum_measurable`](../../GaussianField/Construction.lean#L381)

---

## Isometric Embedding for Finite-Dimensional H

### `hilbertEmbedding` --- Definition (private)

**Lean signature**
```lean
private noncomputable def hilbertEmbedding (hfin : FiniteDimensional ℝ H) : H →L[ℝ] ell2'
```

**Informal**: Isometric embedding of a finite-dimensional $H$ into $\ell^2$ via the standard ONB: $x \mapsto \sum_i \langle b_i, x \rangle e_i$.

---

### [`hilbertEmbedding_inner`](../../GaussianField/Construction.lean#L458) --- Lemma (private)

**Statement**: The embedding preserves inner products: $\langle \iota(x), \iota(y) \rangle_{\ell^2} = \langle x, y \rangle_H$.

**Proof uses**: `stdOrthonormalBasis`, `OrthonormalBasis.repr.inner_map_map`

---

## Measure Definition

### `measure` --- Definition

**Lean signature**
```lean
def measure (T : E →L[ℝ] H) :
    @Measure (Configuration E) instMeasurableSpaceConfiguration
```

**Informal**: The Gaussian probability measure on $E'$ constructed from $T$. For infinite-dimensional $H$, this is the pushforward of the noise measure through the series-limit map. For finite-dimensional $H$, an isometric embedding into $\ell^2$ is used first.

---

### [`measure_isProbability`](../../GaussianField/Construction.lean#L498) --- Theorem

**Statement**: The constructed measure is a probability measure.

**Proof uses**: `Measure.isProbabilityMeasure_map`, [`aemeasurable_seriesLimit`](../../GaussianField/Construction.lean#L399)

---

## Characteristic Functional

### [`partial_sum_charFun`](../../GaussianField/Construction.lean#L582) --- Theorem (private)

**Statement**: The characteristic functional of the $N$-th partial sum equals $\exp\!\bigl(-\tfrac{1}{2} \sum_{k < N} c_k(f)^2\bigr)$, by independence and the 1D Gaussian CF.

**Proof uses**: [`noise_integral_factor`](../../GaussianField/Construction.lean#L535), `charFun_gaussianReal`

---

### [`charFun_noise_integral`](../../GaussianField/Construction.lean#L627) --- Theorem (private)

**Statement**: The noise integral $\int \exp(i \cdot \omega(f))\, d\mu_{\mathrm{noise}}$ equals $\exp(-\tfrac{1}{2}\langle T(f), T(f)\rangle)$. Proved by combining the partial-sum CF with Parseval and dominated convergence.

**Proof uses**: [`coeff_parseval`](../../GaussianField/Construction.lean#L197), [`partial_sum_charFun`](../../GaussianField/Construction.lean#L582), [`partialSum_tendsto`](../../GaussianField/Construction.lean#L509), `tendsto_integral_of_dominated_convergence`

---

### [`charFun`](../../GaussianField/Construction.lean#L687) --- Theorem

**Statement**: **Characteristic functional identity**: $\mathbb{E}[e^{i\langle \omega, f \rangle}] = \exp\!\bigl(-\tfrac{1}{2}\langle T(f), T(f)\rangle_H\bigr)$. For finite-dimensional $H$, proved via the isometric embedding; for infinite-dimensional $H$, via the direct noise integral.

**Proof uses**: [`charFun_noise_integral`](../../GaussianField/Construction.lean#L627), [`hilbertEmbedding_inner`](../../GaussianField/Construction.lean#L458), [`aemeasurable_seriesLimit`](../../GaussianField/Construction.lean#L399), `integral_map`

---

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