Registry · Lemma II.L03 established formalized

II.L03 — Spectral-Germ Equivalence

Spectral decomposition data is equivalent to germ data: knowing the spectral coefficients of a function at a point determines its omega-germ, and conversely.

Book II Part 6 Ch. 31

Dependency Graph

Depends on (4)

Depended on by (2)

Lean Formalization

Module: TauLib.BookII.Hartogs.MutualDetermination

Symbol: Tau.BookII.Hartogs.spectral_germ_check