# `NuclearSVD.lean` — Informal Summary

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

## Overview

Given a sequence $\{y_m\}$ in a separable Hilbert space $K$ with $\sum \lVert y_m \rVert < \infty$, constructs the singular value decomposition of the associated nuclear operator $A : \ell^2 \to K$ defined by $A(e_m) = y_m$. The construction proceeds by: (1) building the nuclear CLM $A$, (2) proving $A$ is compact as a norm-limit of finite-rank operators, (3) applying the spectral theorem to $AA^\dagger$, and (4) extracting the SVD with summable singular values.

## Status

**Main result**: Fully proven

None --- file is sorry-free.

**Length**: 640 lines, 4 definition(s) + 16 theorem(s)/lemma(s)

---

## Section 0: l2 basics

### `ell2'` --- Definition

**Lean signature**
```lean
abbrev ell2' := lp (fun _ : ℕ => ℝ) 2
```

**Informal**: The $\ell^2$ space $\ell^2(\mathbb{N}, \mathbb{R})$ used as the domain of the nuclear operator.

---

### `ell2_basis` --- Definition

**Lean signature**
```lean
def ell2_basis (m : ℕ) : ell2'
```

**Informal**: The $m$-th standard basis vector $e_m \in \ell^2$, defined as `lp.single 2 m 1`.

---

### [`ell2_basis_orthonormal`](../../GaussianField/NuclearSVD.lean#L56) --- Theorem

**Statement**: The standard basis $\{e_m\}$ of $\ell^2$ is orthonormal.

**Proof uses**: `lp.norm_single`, `lp.inner_eq_tsum`

---

### [`ell2_not_finiteDimensional`](../../GaussianField/NuclearSVD.lean#L72) --- Theorem

**Statement**: $\ell^2$ is infinite-dimensional.

**Proof uses**: [`ell2_basis_orthonormal`](../../GaussianField/NuclearSVD.lean#L56), `Orthonormal.linearIndependent`

---

### [`ell2_separableSpace`](../../GaussianField/NuclearSVD.lean#L79) --- Theorem

**Statement**: $\ell^2$ is separable.

**Proof uses**: `lp.hasSum_single`, [`ell2_basis`](../../GaussianField/NuclearSVD.lean#L53)

---

## Section 1: N-indexed Spectral Theorem Corollary

### [`orthonormal_countable'`](../../GaussianField/NuclearSVD.lean#L102) --- Theorem

**Statement**: Orthonormal sets in separable spaces have countable index.

**Proof uses**: `Pairwise.countable_of_isOpen_disjoint`

---

### [`hilbertBasis_fintype_finiteDimensional`](../../GaussianField/NuclearSVD.lean#L124) --- Theorem

**Statement**: If a Hilbert basis has finite index type, then the space is finite-dimensional.

**Proof uses**: `HilbertBasis.dense_span`, `Submodule.closed_of_finiteDimensional`

---

### [`compact_selfAdjoint_spectral_nat`](../../GaussianField/NuclearSVD.lean#L144) --- Theorem

**Statement**: $\mathbb{N}$-indexed corollary of the spectral theorem: for a compact self-adjoint operator on a separable infinite-dimensional Hilbert space, there exists an $\mathbb{N}$-indexed ONB of eigenvectors.

**Proof uses**: [`compact_selfAdjoint_spectral`](../../GaussianField/SpectralTheorem.lean#L451), [`orthonormal_countable'`](../../GaussianField/NuclearSVD.lean#L102), [`hilbertBasis_fintype_finiteDimensional`](../../GaussianField/NuclearSVD.lean#L124), `nonempty_equiv_of_countable`

---

## Section 2: Nuclear Operator Construction

### [`summable_norm_sq_of_summable_norm`](../../GaussianField/NuclearSVD.lean#L178) --- Theorem

**Statement**: $\sum \lVert y_m \rVert < \infty$ implies $\sum \lVert y_m \rVert^2 < \infty$.

**Proof uses**: `Summable.of_norm_bounded_eventually_nat`, `Summable.tendsto_atTop_zero`

---

### [`summable_smul_of_ell2`](../../GaussianField/NuclearSVD.lean#L193) --- Theorem

**Statement**: For $x \in \ell^2$ and $\sum \lVert y_m \rVert < \infty$, the series $\sum x_m y_m$ is summable.

**Proof uses**: `lp.summable_inner`, [`summable_norm_sq_of_summable_norm`](../../GaussianField/NuclearSVD.lean#L178)

---

### `nuclear_linearMap` --- Definition

**Lean signature**
```lean
def nuclear_linearMap (y : ℕ → K) (hy : Summable (fun m => ‖y m‖)) :
    ell2' →ₗ[ℝ] K
```

**Informal**: The linear map underlying the nuclear operator: $A(x) = \sum_m x_m y_m$.

---

### `nuclear_clm` --- Definition

**Lean signature**
```lean
def nuclear_clm (y : ℕ → K) (hy : Summable (fun m => ‖y m‖)) :
    ell2' →L[ℝ] K
```

**Informal**: The nuclear operator $A : \ell^2 \to K$ as a continuous linear map, with $A(e_m) = y_m$.

---

### [`nuclear_clm_basis`](../../GaussianField/NuclearSVD.lean#L250) --- Theorem

**Statement**: The nuclear operator maps standard basis vectors to $y_m$: $A(e_m) = y_m$.

**Proof uses**: `tsum_eq_single`

---

## Section 3: Compactness of Nuclear Operators

### [`nuclear_clm_isCompact`](../../GaussianField/NuclearSVD.lean#L324) --- Theorem

**Statement**: Nuclear operators are compact (as norm-limits of finite-rank operators).

**Proof uses**: [`smulRight_isCompactOperator`](../../GaussianField/NuclearSVD.lean#L283), [`rank1_norm_le`](../../GaussianField/NuclearSVD.lean#L314), `isCompactOperator_of_tendsto`

---

## Section 4: Gram Operator Properties

### [`gram_isSelfAdjoint'`](../../GaussianField/NuclearSVD.lean#L363) --- Theorem

**Statement**: $A^\dagger A$ is self-adjoint.

**Proof uses**: `ContinuousLinearMap.adjoint_comp`, `ContinuousLinearMap.adjoint_adjoint`

---

### [`gram_isCompact'`](../../GaussianField/NuclearSVD.lean#L369) --- Theorem

**Statement**: $A^\dagger A$ is compact when $A$ is compact.

**Proof uses**: `IsCompactOperator.clm_comp`

---

## Section 5: Summability of singular values

### [`summable_sqrt_eigenvalues`](../../GaussianField/NuclearSVD.lean#L379) --- Theorem

**Statement**: The singular values $\sigma_n = \sqrt{\mu_n}$ are summable: $\sum_n \sigma_n < \infty$. Proved via a Cauchy--Schwarz argument bounding $\sum_{n \in S} \sigma_n \le \sum_m \lVert y_m \rVert$ for all finite $S$.

**Proof uses**: [`inner_ell2_basis_eq_coord`](../../GaussianField/NuclearSVD.lean#L268), `lp.hasSum_inner`, `Finset.sum_mul_sq_le_sq_mul_sq`

---

## Section 6: Main Theorem

### [`nuclear_sequence_svd`](../../GaussianField/NuclearSVD.lean#L515) --- Theorem

**Statement**: **Nuclear sequence SVD**: Given $\{y_m\}$ with $\sum \lVert y_m \rVert < \infty$ in a separable infinite-dimensional Hilbert space, there exist an ONB $\{e_n\}$, singular values $\sigma_n \ge 0$ with $\sum \sigma_n < \infty$, and an orthogonal matrix $W$ such that $\langle e_n, y_m \rangle = \sigma_n W_{nm}$.

**Proof uses**: [`nuclear_clm`](../../GaussianField/NuclearSVD.lean#L243), [`nuclear_clm_isCompact`](../../GaussianField/NuclearSVD.lean#L324), [`compact_selfAdjoint_spectral_nat`](../../GaussianField/NuclearSVD.lean#L144), [`summable_sqrt_eigenvalues`](../../GaussianField/NuclearSVD.lean#L379), `lp.hasSum_inner`

---

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