`IndisputableMonolith.Quantum.HilbertSpace`

IndisputableMonolith/Quantum/HilbertSpace.lean · 26 lines · 2 declarations

Explainer status: pending

   1import Mathlib.Analysis.InnerProductSpace.Basic
   2import Mathlib.Analysis.InnerProductSpace.Projection.Basic
   3import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
   4import Mathlib.Analysis.InnerProductSpace.Projection.Minimal
   5import Mathlib.Analysis.InnerProductSpace.Projection.Reflection
   6import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
   7import Mathlib.Topology.Bases
   8
   9/-! # Hilbert Space for Recognition Science QM Bridge -/
  10
  11namespace IndisputableMonolith.Quantum
  12
  13/-- A separable Hilbert space structure -/
  14class RSHilbertSpace (H : Type*) extends
  15  SeminormedAddCommGroup H,
  16  InnerProductSpace ℂ H,
  17  CompleteSpace H,
  18  TopologicalSpace.SeparableSpace H
  19
  20/-- Normalized state (unit vector) -/
  21structure NormalizedState (H : Type*) [RSHilbertSpace H] where
  22  vec : H
  23  norm_one : ‖vec‖ = 1
  24
  25end IndisputableMonolith.Quantum
  26

source mirrored from github.com/jonwashburn/shape-of-logic