ConcreteTraceTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Strong trace transfer in a concrete finite representation

A finite vector-functional formula for the trace is enough: weak compactness of the positive operator ball and faithfulness prove the uniform two-norm-to-strong implication. No transfer theorem is assumed.

def OAI.KadisonKastler.FiniteVectorTrace line 29
Source documentation
A finite vector-functional formula, used below for the factor trace.
```
def FiniteVectorTrace (τ : FaithfulTracialState (Algebra M)) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.FiniteVectorTrace.tendsto line 33
theorem OAI.KadisonKastler.FiniteVectorTrace.strongContinuous line 45
Source documentation
Faithfulness and weak compactness turn the normal trace into a uniform strong-topology control on each operator-norm ball.
```
theorem FiniteVectorTrace.strongContinuous {τ : FaithfulTracialState (Algebra M)}
    (hτ : FiniteVectorTrace τ) : TraceStrongContinuous τ M.toStarSubalgebra.subtype := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.TraceStrongContinuous