ConcreteTraceUniqueness.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of the normalized faithful factor trace

Projection dimension identifies any positive normalized tracial functional on a finite diffuse factor. In particular, the explicit matrix trace agrees with the canonical ultrapower trace.

def OAI.KadisonKastler.FaithfulTracialState.toContinuousLinearMap line 18
theorem OAI.KadisonKastler.FaithfulTracialState.norm_toContinuousLinearMap_le line 21
theorem OAI.KadisonKastler.FaithfulTracialState.nonneg line 32
theorem OAI.KadisonKastler.scalarCenter line 47
theorem OAI.KadisonKastler.one_ne_zero line 53
theorem OAI.KadisonKastler.trace_on_selfAdjoint line 56
theorem OAI.KadisonKastler.faithfulTracialState_unique line 71
Source documentation
Any two normalized faithful tracial states on a concrete II1 factor agree. Normality is not an extra premise.
```
theorem faithfulTracialState_unique
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τ σ : FaithfulTracialState (Algebra M)) (x : Algebra M) :
    τ.toLinearMap x = σ.toLinearMap x := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.faithfulTracialState_eq_concreteFactorTrace line 83
Source documentation
The explicit normalized matrix trace therefore equals the canonical trace selected by the concrete factor construction.
```
theorem faithfulTracialState_eq_concreteFactorTrace
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τ : FaithfulTracialState (Algebra M)) (x : Algebra M) :
    τ.toLinearMap x = (concreteFactorTrace hM).toLinearMap x :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteFactorTrace