Registry · Definition I.D65 tau-effective formalized

I.D65 — Spectral Coefficients

Spectral coefficients of a StageFun at input n, stage k: the B-sector and C-sector outputs. Together they fully determine the function value.

Book I Part 16 Ch. 60

Dependency Graph

Depends on (3)

I.D47 I.D37 I.T21

Depended on by (1)

I.T29

Lean Formalization

Module: TauLib.BookI.Holomorphy.SpectralCoefficients

Symbol: Tau.Holomorphy.SpectralCoeff