Registry · Definition IV.D62 tau-effective formalized

IV.D62 — Holomorphic Hilbert Space

H_τ = L²-completion of CR(τ³). The quantum state space, obtained by completing the pre-Hilbert space of CR-functions.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (3)

IV.D60 IV.D61 IV.P17

Depended on by (11)

IV.D63 IV.D64 IV.D66 IV.D67 IV.P19 IV.P20 IV.P21 IV.P22 IV.T18 IV.T19 IV.T20

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.HolomorphicHilbertSpace