ConcreteWeakTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Weak tracial transfer along an ultrafilter

Weak compactness and the concrete finite-vector trace formula identify operator ultralimits from their tracial pairings. No Radon–Nikodym or trace-dual density hypothesis is added.

theorem OAI.KadisonKastler.FiniteVectorTrace.weakOperator_ultralimit line 24

Source documentation

On a bounded family, convergence of all tracial pairings determines the weak operator ultralimit in the original concrete representation.

theorem FiniteVectorTrace.weakOperator_ultralimit
    {τ : FaithfulTracialState (Algebra M)} (hτ : FiniteVectorTrace τ)
    {J : Type*} (ω : Ultrafilter J) (x : J → Algebra M) (a : Algebra M)
    {C : ℝ} (hC : 0 ≤ C) (hx : ∀ j, ‖x j‖ ≤ C)
    (htrace : ∀ b : Algebra M,
      Tendsto (fun j => τ.toLinearMap (b * x j)) (ω : Filter J)
        (𝓝 (τ.toLinearMap (b * a)))) :
    ∀ ξ η : H, Tendsto (fun j => inner ℂ η ((x j : H →L[ℂ] H) ξ))
      (ω : Filter J) (𝓝 (inner ℂ η ((a : H →L[ℂ] H) ξ))) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace