ConcreteFiniteTrace.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The faithful normal trace of a concrete finite diffuse factor

The projection-dimension trace gives a faithful normal tracial state on a concrete finite diffuse factor.

theorem OAI.KadisonKastler.factor_central line 24
theorem OAI.KadisonKastler.factor_one_ne_zero line 30
def OAI.KadisonKastler.concreteFactorTrace line 37
Source documentation
The trace is a complex-valued faithful tracial state with the continuity required by amplification.
```
def concreteFactorTrace (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    FaithfulTracialState (Algebra M) where
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.concreteFactorTrace_finiteVector line 63
Source documentation
Its finite vector-functional expression is also already proved in the concrete representation in which the factor was supplied.
```
theorem concreteFactorTrace_finiteVector (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    FiniteVectorTrace (concreteFactorTrace hM) := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.concreteFactorTrace
theorem OAI.KadisonKastler.concreteFactorTrace_strongContinuous line 71
Source documentation
The normal trace transfers two-small bounded elements to strongly small operators in the original concrete representation.
```
theorem concreteFactorTrace_strongContinuous (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    TraceStrongContinuous (concreteFactorTrace hM) M.toStarSubalgebra.subtype :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.TraceStrongContinuous, OAI.KadisonKastler.concreteFactorTrace