# `NuclearFactorization.lean` — Informal Summary

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

## Overview

For any continuous linear map $T : E \to H$ from a nuclear Frechet space (a `DyninMityaginSpace`) to a Hilbert space, produces a nuclear representation $T(f) = \sum_m \varphi_m(f) \cdot y_m$ with $\sum_m \lVert y_m \rVert < \infty$, where $\varphi_m$ are equicontinuous coefficient functionals. The proof uses the Schauder basis expansion, polynomial growth of $\lVert T(\psi_m) \rVert$, and a renormalization trick with exponent $s = p_1 + 2$ to ensure $\ell^1$ convergence.

## Status

**Main result**: Fully proven

None --- file is sorry-free.

**Length**: 191 lines, 0 definition(s) + 5 theorem(s)/lemma(s)

---

## P-series summability helper

### [`summable_one_add_rpow_neg_two`](../../GaussianField/NuclearFactorization.lean#L47) --- Lemma

**Statement**: The series $\sum_{m=0}^\infty (1+m)^{-2}$ converges (p-series test).

**Proof uses**: `Real.summable_nat_rpow`

---

## Polynomial growth of CLM images on basis

### [`clm_image_growth`](../../GaussianField/NuclearFactorization.lean#L100) --- Theorem

**Statement**: For a CLM $T : E \to H$, the images of basis elements grow polynomially: there exist $C > 0$ and $p_1 \in \mathbb{N}$ such that $\lVert T(\psi_m) \rVert \le C (1+m)^{p_1}$ for all $m$.

**Proof uses**: `Seminorm.bound_of_continuous`, `DyninMityaginSpace.basis_growth`, [`finset_sup_seminorm_poly_bound`](../../GaussianField/NuclearFactorization.lean#L58)

---

## Nuclear representation theorem

### [`nuclear_clm_representation`](../../GaussianField/NuclearFactorization.lean#L134) --- Theorem

**Statement**: **Nuclear representation**: Any CLM $T : E \to H$ from a nuclear space to a Hilbert space admits a representation $\langle w, T(f) \rangle = \sum_m \varphi_m(f) \langle w, y_m \rangle$ with $\sum_m \lVert y_m \rVert < \infty$ and the $\varphi_m$ equicontinuous (bounded by a single seminorm).

**Proof uses**: [`clm_image_growth`](../../GaussianField/NuclearFactorization.lean#L100), [`summable_one_add_rpow_neg_two`](../../GaussianField/NuclearFactorization.lean#L47), `DyninMityaginSpace.coeff_decay`, `DyninMityaginSpace.expansion_H`

---

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