Registry · Definition IV.D61 tau-effective formalized

IV.D61 — Canonical Inner Product

⟨f,g⟩ = ∫_{τ³} f̄·g dμ where dμ is the fibered product measure with μ(T²) = 1.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (1)

IV.D60

Depended on by (5)

IV.D348 IV.D62 IV.P17 IV.P18 IV.P24

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.CanonicalInnerProduct