# `NuclearSpace.lean` — Informal Summary

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

## Overview

Defines nuclear operators, Hilbertian seminorms (via the parallelogram law), Hilbert-Schmidt embeddings between seminorm completions, and nuclear spaces as locally convex spaces whose topology is generated by a countable chain of Hilbertian seminorms with Hilbert-Schmidt inclusions. Also equips `WeakDual ℝ E` with the cylinder $\sigma$-algebra generated by evaluation maps and proves those evaluations are measurable. Adapted from OSforGFF/IsHilbertNuclear.lean.

## Status

**Main result**: `IsHilbertNuclear` -- typeclass capturing nuclear spaces via Hilbert-Schmidt chains of Hilbertian seminorms.
**Length**: 99 lines, 7 definition(s) + 1 theorem(s)/lemma(s)

---

### [`IsNuclearMap`](../../Minlos/NuclearSpace.lean#L30)

```lean
def IsNuclearMap {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
    (T : E →L[ℝ] F) : Prop
```

A continuous linear map $T : E \to F$ between normed spaces is **nuclear** if there exist sequences $(\varphi_n)$ in $E^*$ and $(y_n)$ in $F$ with $\sum_n \lVert \varphi_n \rVert \cdot \lVert y_n \rVert < \infty$ such that $T(x) = \sum_n \varphi_n(x) \, y_n$ for all $x$.

---

### [`Seminorm.IsHilbertian`](../../Minlos/NuclearSpace.lean#L42)

```lean
def Seminorm.IsHilbertian {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p : Seminorm ℝ E) : Prop
```

A seminorm $p$ on $E$ is **Hilbertian** (i.e., arises from an inner product) iff it satisfies the parallelogram law:
$$p(x+y)^2 + p(x-y)^2 = 2\bigl(p(x)^2 + p(y)^2\bigr).$$

---

### [`Seminorm.innerProd`](../../Minlos/NuclearSpace.lean#L47)

```lean
noncomputable def Seminorm.innerProd {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p : Seminorm ℝ E) (x y : E) : ℝ
```

The inner product induced by a Hilbertian seminorm $p$ via polarization:
$$\langle x, y \rangle_p \;=\; \frac{p(x+y)^2 - p(x-y)^2}{4}.$$

---

### [`Seminorm.IsOrthonormalSeq`](../../Minlos/NuclearSpace.lean#L52)

```lean
def Seminorm.IsOrthonormalSeq {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p : Seminorm ℝ E) {n : ℕ} (e : Fin n → E) : Prop
```

A finite sequence $(e_0, \ldots, e_{n-1})$ in $E$ is **$p$-orthonormal** if $\langle e_i, e_j \rangle_p = \delta_{ij}$ for all $i, j$.

---

### [`Seminorm.IsHilbertSchmidtEmbedding`](../../Minlos/NuclearSpace.lean#L60)

```lean
def Seminorm.IsHilbertSchmidtEmbedding {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p q : Seminorm ℝ E) : Prop
```

The canonical inclusion $\hat{E}_p \hookrightarrow \hat{E}_q$ (between seminorm completions) is **Hilbert-Schmidt**: $q \le p$ and there exists $C$ such that for every finite $p$-orthonormal sequence $(e_k)_{k < n}$,
$$\sum_{k=0}^{n-1} q(e_k)^2 \;\le\; C.$$

---

### [`IsHilbertNuclear`](../../Minlos/NuclearSpace.lean#L74)

```lean
class IsHilbertNuclear (E : Type*) [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] : Prop
```

A locally convex space $E$ is a **nuclear space** (in the Hilbertian sense) if its topology is generated by a countable family of Hilbertian seminorms $(p_n)_{n \in \mathbb{N}}$ such that for every $n$, the inclusion $\hat{E}_{p_{n+1}} \hookrightarrow \hat{E}_{p_n}$ is Hilbert-Schmidt. Reference: Treves, *Topological Vector Spaces*, Ch. 50, Thm 50.1.

---

### [`MeasurableSpace (WeakDual ℝ E)`](../../Minlos/NuclearSpace.lean#L89) (instance)

```lean
instance : MeasurableSpace (WeakDual ℝ E) :=
  ⨆ (f : E), (borel ℝ).comap (fun l : WeakDual ℝ E => (l : E →L[ℝ] ℝ) f)
```

The **cylinder $\sigma$-algebra** on $E'_w = \mathrm{WeakDual}\;\mathbb{R}\;E$, generated by all evaluation maps $l \mapsto l(f)$ for $f \in E$. For separable nuclear spaces this coincides with the Borel $\sigma$-algebra (Bogachev, *Gaussian Measures*, Thm 3.6.1).

---

### [`WeakDual.eval_measurable`](../../Minlos/NuclearSpace.lean#L93)

Each evaluation map $l \mapsto l(f)$ is measurable with respect to the cylinder $\sigma$-algebra on $\mathrm{WeakDual}\;\mathbb{R}\;E$.

**Proof.** The cylinder $\sigma$-algebra is the supremum $\bigvee_f (\mathrm{borel}\;\mathbb{R}).\mathrm{comap}(\mathrm{eval}_f)$. For a fixed $f$, the comap of $\mathrm{eval}_f$ is by definition $\le$ this supremum (`le_iSup`), which is exactly the condition `measurable_iff_comap_le`.

**Dependencies**: `measurable_iff_comap_le`, `le_iSup`.

---

*This file has **7** definitions and **1** theorem/lemma (0 with sorry).*