FiniteTraceWeakLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Ambient projections detected by a finite normal trace

The trace need only have a finite vector-functional expression. Uniform contractivity and convergence in its two-norm suffice on the original space.

theorem OAI.KadisonKastler.isInjective_of_finiteTrace_approximations line 23

Source documentation

The finite-vector trace replaces a separating trace vector in the weak-limit construction.

theorem isInjective_of_finiteTrace_approximations
    (hQM : Q ≤ M) (τ : FaithfulTracialState (Algebra M)) (hτ : FiniteVectorTrace τ)
    (F : ℕ → (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hF : ∀ n, ‖F n‖ ≤ 1) (hmem : ∀ n T, F n T ∈ Q)
    (hfix : ∀ a : Algebra Q, Tendsto
      (fun n => traceTwoNorm τ
        ((⟨F n a.val,hQM (hmem n a.val)⟩ : Algebra M) - coordinateInclusion hQM a))
      atTop (𝓝 0)) : IsInjective Q := by
…

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