Registry · Theorem IV.T19 tau-effective formalized

IV.T19 — Orthonormal Basis

{χ_{m,n} : (m,n) ∈ Λ_CR} is an orthonormal basis for H_τ. Orthonormality from Haar; completeness from Peter-Weyl restricted to CR-sublattice.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (4)

IV.D62 IV.D54 IV.T18 IV.P19

Depended on by (1)

IV.P20

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.OrthonormalBasis