Registry · Proposition IV.P20 tau-effective formalized

IV.P20 — Spectral Completeness

Every f ∈ H_τ decomposes uniquely as f = Σ c_{m,n} χ_{m,n} with convergence in the H_τ norm.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.SpectralCompleteness