TraceSeparability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Trace separability in a separably acting finite representation

A finite vector formula bounds the trace two-norm by finitely many Hilbert-space coordinates. Countable dense subsets of their ranges lift to countable two-norm dense subsets of any prescribed set of operators.

def OAI.KadisonKastler.traceCoordinates line 23
theorem OAI.KadisonKastler.traceTwoNorm_le_coordinates line 33
theorem OAI.KadisonKastler.FiniteVectorTrace.traceSeparable line 66
Source documentation
Every subset of a separably acting finite representation is separable for its faithful trace two-norm.
```
theorem FiniteVectorTrace.traceSeparable [SeparableSpace H]
    {τ : FaithfulTracialState (Algebra M)} (hτ : FiniteVectorTrace τ)
    (S : Set (Algebra M)) : TraceSeparable τ S := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.TraceSeparable