GNSHilbertStructure.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Bundled GNS spaces keep the canonical Hilbert structures explicit when specializing to concrete represented corners.

def OAI.WeakPureInfiniteness.gnsHilbert line 16
Source documentation
The usual GNS Hilbert space, with its existing canonical structures.
```
def gnsHilbert (φ : A →ₚ[ℂ] ℂ) : ComplexHilbert where
…
```
Mentions: OAI.WeakPureInfiniteness.ComplexHilbert

def OAI.WeakPureInfiniteness.cyclicBundledGNSIsometry line 22

Source documentation

The cyclic isometry with a bundled source Hilbert space.

def cyclicBundledGNSIsometry (φ : A →ₚ[ℂ] ℂ) (π : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ξ : H) (hφ : ∀ a, φ a = inner ℂ ξ (π a ξ)) :
    gnsHilbert φ →ₗᵢ[ℂ] H := cyclicGNSIsometry φ π ξ hφ

Mentions: OAI.WeakPureInfiniteness.gnsHilbert, OAI.WeakPureInfiniteness.cyclicGNSIsometry

lemma OAI.WeakPureInfiniteness.cyclicBundledGNSIsometry_vector line 26

def OAI.WeakPureInfiniteness.normalizedCornerGNSInclusion line 35

Source documentation

A normalized corner vector realizes the state on its GNS space.

def normalizedCornerGNSInclusion (V : K →ₗᵢ[ℂ] H) (φ : A →ₚ[ℂ] ℂ)
    (π : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (z : H)
    (hφ : ∀ a, φ a = inner ℂ
      (((‖z‖⁻¹ : ℝ) : ℂ) • V.toContinuousLinearMap.adjoint z)
      (π a (((‖z‖⁻¹ : ℝ) : ℂ) • V.toContinuousLinearMap.adjoint z))) :
    gnsHilbert φ →ₗᵢ[ℂ] H :=
…

Mentions: OAI.WeakPureInfiniteness.gnsHilbert

lemma OAI.WeakPureInfiniteness.normalizedCornerGNSInclusion_vector line 44