# `SpectralTheorem.lean` — Informal Summary

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

## Overview

Proves the spectral theorem for compact self-adjoint operators on real Hilbert spaces with no custom axioms. The key steps are: (1) eigenvector existence via a maximizing sequence and the $T^2$ trick, (2) eigenspaces span by a restrict-to-complement argument, and (3) a Zorn-based construction of a full eigenvector Hilbert basis. All results are fully proved using only Mathlib.

## Status

**Main result**: Fully proven

None --- file is sorry-free.

**Length**: 468 lines, 0 definition(s) + 6 theorem(s)/lemma(s)

---

## Helper: Eigenvector existence (explicit form)

### [`hasEigenvector_aux`](../../GaussianField/SpectralTheorem.lean#L55) --- Theorem (private)

**Statement**: A nonzero compact self-adjoint operator $T$ on a nontrivial real Hilbert space has an eigenvector with eigenvalue $\mu$ satisfying $\lvert \mu \rvert = \lVert T \rVert$.

**Proof uses**: `ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric`, `ContinuousLinearMap.exists_lt_apply_of_lt_opNorm`, `IsCompact.isSeqCompact`, `tendsto_one_div_add_atTop_nhds_zero_nat`

---

## Theorem 1: Eigenvector existence

### [`compact_selfAdjoint_hasEigenvector`](../../GaussianField/SpectralTheorem.lean#L223) --- Theorem

**Statement**: A compact self-adjoint operator on a nontrivial real Hilbert space has an eigenvalue $\mu$ with $\lvert \mu \rvert = \lVert T \rVert$.

**Proof uses**: [`hasEigenvector_aux`](../../GaussianField/SpectralTheorem.lean#L55), `Module.End.HasEigenvalue`, `Module.End.mem_eigenspace_iff`

---

## Theorem 2: Eigenspaces span

### [`compact_selfAdjoint_orthogonalComplement_iSup_eigenspaces_eq_bot`](../../GaussianField/SpectralTheorem.lean#L239) --- Theorem

**Statement**: The orthogonal complement of the span of all eigenspaces of a compact self-adjoint operator is $\{0\}$: $\bigl(\bigoplus_\mu E_\mu\bigr)^\perp = \bot$.

**Proof uses**: `LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant`, `LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces`, [`hasEigenvector_aux`](../../GaussianField/SpectralTheorem.lean#L55), `IsCompactOperator.comp_clm`, `IsCompactOperator.codRestrict`

---

## Helper: Eigenvector Hilbert basis (Zorn construction)

### [`eigenvector_basis`](../../GaussianField/SpectralTheorem.lean#L308) --- Theorem (private)

**Statement**: Every compact self-adjoint operator admits a Hilbert basis of eigenvectors. Constructed via Zorn's lemma applied to maximal orthonormal subsets of eigenvectors.

**Proof uses**: [`compact_selfAdjoint_orthogonalComplement_iSup_eigenspaces_eq_bot`](../../GaussianField/SpectralTheorem.lean#L239), [`hasEigenvector_aux`](../../GaussianField/SpectralTheorem.lean#L55), `zorn_subset_nonempty`, `orthonormal_sUnion_of_directed`, `HilbertBasis.mkOfOrthogonalEqBot`

---

## Theorem 3: Spectral theorem (diagonal representation)

### [`compact_selfAdjoint_spectral`](../../GaussianField/SpectralTheorem.lean#L451) --- Theorem

**Statement**: **Spectral Theorem**: Every compact self-adjoint operator $T$ on a real Hilbert space admits a Hilbert basis $\{e_\iota\}$ of eigenvectors with eigenvalues $\mu_\iota$ such that $T(x) = \sum_\iota \mu_\iota \langle e_\iota, x \rangle e_\iota$ (norm-convergent).

**Proof uses**: [`eigenvector_basis`](../../GaussianField/SpectralTheorem.lean#L308), `HilbertBasis.hasSum_repr`, `HasSum.mapL`, `HilbertBasis.repr_apply_apply`

---

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