# `TargetFactorization.lean` — Informal Summary

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

## Overview

Combines the source-indexed nuclear representation (from `NuclearFactorization.lean`) with the nuclear SVD (from `NuclearSVD.lean`) to produce a target-indexed factorization of any CLM $T : E \to H$ from a nuclear Frechet space into a separable infinite-dimensional Hilbert space. The result gives an adapted ONB $\{e_n\}$ of $H$, an intermediate Hilbert space $K = \ell^2$, a CLM $j : E \to K$, and vectors $v_n \in K$ with $\sum \lVert v_n \rVert < \infty$ such that $\langle e_n, T(f) \rangle_H = \langle v_n, j(f) \rangle_K$. This factorization drives the Gaussian measure construction.

## Status

**Main result**: Fully proven

None --- file is sorry-free.

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

---

## l2 Construction Helpers

### [`ell2_inner_eq_tsum`](../../GaussianField/TargetFactorization.lean#L43) --- Theorem

**Statement**: The $\ell^2$ inner product equals the tsum of coordinate products: $\langle x, y \rangle_{\ell^2} = \sum_m x_m y_m$.

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

---

### [`summable_smul_ell2`](../../GaussianField/TargetFactorization.lean#L49) --- Theorem

**Statement**: If $\sum \sigma_n < \infty$ with $\sigma_n \ge 0$ and $\lVert u_n \rVert = 1$ when $\sigma_n \ne 0$, then $\sum \lVert \sigma_n u_n \rVert < \infty$.

**Proof uses**: *(direct tactic proof)*

---

## l2 embedding from decay

### [`nuclear_ell2_embedding_from_decay`](../../GaussianField/TargetFactorization.lean#L68) --- Theorem

**Statement**: Given CLMs $\varphi_m : E \to \mathbb{R}$ satisfying $\lvert \varphi_m(f) \rvert \le C \cdot p_q(f) \cdot (1+m)^{-2}$, the map $j(f) = (\varphi_m(f))_m$ defines a CLM $j : E \to \ell^2$ with $(j(f))_m = \varphi_m(f)$.

**Proof uses**: `Seminorm.cont_withSeminorms_normedSpace`, `DyninMityaginSpace.h_with`, `Real.summable_nat_rpow`

---

## Main Theorem

### [`nuclear_clm_target_factorization`](../../GaussianField/TargetFactorization.lean#L196) --- Theorem

**Statement**: **Target-indexed nuclear factorization**: Any CLM $T : E \to H$ from a nuclear Frechet space into a separable infinite-dimensional Hilbert space admits a factorization: there exist an adapted ONB $\{e_n\}$ of $H$, an intermediate Hilbert space $K$, a CLM $j : E \to K$, and vectors $v_n \in K$ with $\sum \lVert v_n \rVert < \infty$ such that $\langle e_n, T(f) \rangle_H = \langle v_n, j(f) \rangle_K$ for all $f$ and $n$.

**Proof uses**: [`clm_image_growth`](../../GaussianField/NuclearFactorization.lean#L100), [`nuclear_sequence_svd`](../../GaussianField/NuclearSVD.lean#L515), [`nuclear_ell2_embedding_from_decay`](../../GaussianField/TargetFactorization.lean#L68), `DyninMityaginSpace.coeff_decay`, `DyninMityaginSpace.expansion_H`, `lp.inner_eq_tsum`

---

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