Registry · Definition III.D82 tau-effective formalized

III.D82 — Spectral Measure

Spectral measure μ_spec assigns weight 1/N to each eigenvalue λ_n. Total measure = 1 (all modes counted). Counting measure on the discrete spectrum.

Book III Part 4 Ch. 30

Dependency Graph

Depends on (1)

III.D81

Depended on by (1)

III.T56

Lean Formalization

Module: TauLib.BookIII.Doors.SpectralDecomp

Symbol: spectral_measure