TracialGeneratedNormalClosure.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Membership in a concrete finite von Neumann subalgebra is detected by its closed space of trace vectors. This identifies the normal range of the bounded tracially generated algebra.

def OAI.KadisonSimilarity.subalgebraTraceVectors line 18
Source documentation
The trace-vector image of a concrete subalgebra.
```
def subalgebraTraceVectors (τ : TracialRepresentation M) (N : VonNeumannAlgebra H) : Set H :=
…
```
theorem OAI.KadisonSimilarity.mem_of_traceVector_mem_closure line 23
Source documentation
Orthogonality of the conditional expectation detects membership from the closed trace-vector space, without a uniform bound on approximants.
```
theorem mem_of_traceVector_mem_closure (τ : TracialRepresentation M) (hNM : N ≤ M)
    (x : M.toStarSubalgebra)
    (hx : baseVector τ x ∈ closure (subalgebraTraceVectors τ N)) :
    (x : H →L[ℂ] H) ∈ N := by
…
```
Mentions: OAI.KadisonSimilarity.subalgebraTraceVectors
theorem OAI.KadisonSimilarity.mem_iff_traceVector_mem_closure line 55