ConcreteGNSNormality.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A trace realized faithfully in a concrete finite von Neumann algebra has normal native GNS range. The original trace vector need not be cyclic.

def OAI.KadisonSimilarity.HasNormalGNS line 15
Source documentation
Normality of the native representation of the chosen positive trace.
```
def HasNormalGNS {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
    (τ : A →ₚ[ℂ] ℂ) : Prop :=
…
```
theorem OAI.KadisonSimilarity.concreteTraceVector_norm line 30
def OAI.KadisonSimilarity.concreteGNSIsometry line 39
Source documentation
The native GNS space embeds isometrically into the concrete trace space.
```
def concreteGNSIsometry : τ.GNS →ₗᵢ[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.concreteGNSIsometry_vector line 43
theorem OAI.KadisonSimilarity.concrete_gns_trace_balls_closed line 50
Source documentation
Weak-operator bounded limits yield closed native GNS trace-vector balls.
```
theorem concrete_gns_trace_balls_closed (C : ℝ) :
    IsClosed (gnsTracialVector τ '' Metric.closedBall (0 : A) C) := by
…
```
Mentions: OAI.KadisonSimilarity.gnsTracialVector
theorem OAI.KadisonSimilarity.concrete_gns_normal_range line 77
Source documentation
A concrete normal trace gives normality of its native left action.
```
theorem concrete_gns_normal_range :
    τ.gnsStarAlgHom.range = (representationVonNeumannAlgebra τ.gnsStarAlgHom).toStarSubalgebra := by
…
```
Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra