Registry · Theorem III.T56 tau-effective formalized

III.T56 — Parseval Identity

Parseval identity: ‖f‖² = Σ_n |⟨f,e_n⟩|². The Pythagorean theorem for orthogonal spectral decomposition. Verified for test functions at N=2,6.

Book III Part 4 Ch. 30

Dependency Graph

Depends on (2)

III.D81 III.D82

Depended on by (1)

III.P33

Lean Formalization

Module: TauLib.BookIII.Doors.SpectralDecomp

Symbol: parseval_6