TraceVectorTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Trace-to-strong transfer from norm-density of tracial functionals

This proves the analytic transfer argument from the concrete functional approximation property. Existence of this approximation for a normal representation is not asserted here.

def OAI.KadisonKastler.TraceVectorApproximation line 21
Source documentation
Norm approximation of every vector functional by a trace functional. The order of the inner product makes the vector functional complex-linear.
```
def TraceVectorApproximation (τ : FaithfulTracialState B)
    (ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.trace_positive_square_functional_le line 28
Source documentation
Cauchy–Schwarz bounds the trace functional on a positive square by its two-norm and the ambient bound.
```
theorem trace_positive_square_functional_le (τ : FaithfulTracialState B) (b x : B) :
    ‖τ.toLinearMap (b * (star x * x))‖ ≤ ‖b‖ * ‖x‖ * traceTwoNorm τ x := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.TraceVectorApproximation.strongContinuous line 42
Source documentation
Norm-density of the trace functionals implies strong continuity of the tracial two-norm on every bounded ball.
```
theorem TraceVectorApproximation.strongContinuous
    {τ : FaithfulTracialState B} {ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)}
    (h : TraceVectorApproximation τ ρ) : TraceStrongContinuous τ ρ := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceVectorApproximation, OAI.KadisonKastler.TraceStrongContinuous