WeakTraceTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weak operator convergence from tracial pairings

def OAI.KadisonKastler.TracePairingApproximation line 19
Source documentation
The norm-density property for arbitrary vector functionals.
```
def TracePairingApproximation (τ : FaithfulTracialState B)
    (ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.TracePairingApproximation.vector line 24

theorem OAI.KadisonKastler.TracePairingApproximation.weakOperatorConverges line 31

Source documentation

On a bounded set, convergence of all trace pairings implies weak operator convergence in any representation with the density property.

theorem TracePairingApproximation.weakOperatorConverges
    {τ : FaithfulTracialState B} {ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)}
    (h : TracePairingApproximation τ ρ)
    (l : Filter J) (x : J → B) (a : B) {C : ℝ} (hC : 0 ≤ C)
    (hx : ∀ j, ‖x j‖ ≤ C)
    (htrace : ∀ b : B, Tendsto (fun j => τ.toLinearMap (b * x j)) l
      (𝓝 (τ.toLinearMap (b * a)))) :
    WeakOperatorConverges l (fun j => ρ (x j)) (ρ a) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TracePairingApproximation, OAI.KadisonKastler.WeakOperatorConverges