OAI/Analysis/KadisonKastler/TraceProjectionLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.FiniteVectorTrace.projection_limit line 20

   Source documentation

   Selfadjoint contractive two-Cauchy sequences with vanishing idempotency defect converge to a projection in the original algebra.

   theorem FiniteVectorTrace.projection_limit
       {τ : FaithfulTracialState (Algebra M)} (hτ : FiniteVectorTrace τ)
       (x : ℕ → Algebra M) (hx : ∀ j, ‖x j‖ ≤ 1)
       (hsa : ∀ j, IsSelfAdjoint (x j))
       (hCauchy : ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N,
         traceTwoNorm τ (x m - x n) < ε)
       (hdefect : Tendsto (fun j => traceTwoNorm τ (x j * x j - x j)) atTop (𝓝 0)) :
       ∃ e : Algebra M, IsStarProjection e ∧ ‖e‖ ≤ 1 ∧
         (∀ ξ, Tendsto (fun j => (x j : H →L[ℂ] H) ξ) atTop
           (𝓝 ((e : H →L[ℂ] H) ξ))) ∧
         Tendsto (fun j => traceTwoNorm τ (x j - e)) atTop (𝓝 0) := by
   …

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