Physlib.QuantumMechanics.OperatorAlgebra.HilbertSpace

Bounded operators on Hilbert space

This file connects the abstract operator-algebraic quantum-mechanics API with the concrete C⋆-algebra of bounded operators on a complex Hilbert space. The C⋆-algebra, Loewner order, and ordered-star-ring instances for bounded operators are supplied by Mathlib.

2 declarations

definition

Space of bounded operators $B(H)$ on a Hilbert space

#termB(_)

The notation $B(H)$ represents the space of bounded (continuous) linear operators from a complex Hilbert space $H$ to itself, denoted in Lean as `H →L[ℂ] H`.

instance

$\mathcal{B}(\mathcal{H})$ is an `OperatorAlgebra`

#instOperatorAlgebraBoundedOperators

The space of bounded linear operators $\mathcal{B}(\mathcal{H})$ on a complex Hilbert space $\mathcal{H}$ is equipped with the structure of an `OperatorAlgebra`. This instance links the concrete $C^*$ -algebra of bounded operators provided by Mathlib to the abstract operator-algebraic API used in quantum mechanics.

Physlib.QuantumMechanics.OperatorAlgebra.HilbertSpace

Bounded operators on Hilbert space

Space of bounded operators B(H)B(H)B(H) on a Hilbert space

B(H)\mathcal{B}(\mathcal{H})B(H) is an `OperatorAlgebra`

Space of bounded operators $B(H)$ on a Hilbert space

$\mathcal{B}(\mathcal{H})$ is an `OperatorAlgebra`