ConcreteTraceComplete.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Completeness of bounded tracial two-norm balls

Strong trace transfer and Hilbert-space completeness retain tracial limits in the von Neumann algebra, allowing continuous circle cutoffs to converge to spectral projections.

theorem OAI.KadisonKastler.FiniteVectorTrace.traceTwoNorm_tendsto_of_strong line 24

Source documentation

On a bounded operator ball the finite-vector trace is continuous for strong convergence, also in the tracial two-norm.

theorem FiniteVectorTrace.traceTwoNorm_tendsto_of_strong
    {τ : FaithfulTracialState (Algebra M)} (hτ : FiniteVectorTrace τ)
    {J : Type*} {l : Filter J} (x : J → Algebra M) (a : Algebra M)
    {C : ℝ} (hx : ∀ j, ‖x j‖ ≤ C)
    (hstrong : ∀ ξ, Tendsto (fun j => (x j : H →L[ℂ] H) ξ) l
      (𝓝 ((a : H →L[ℂ] H) ξ))) :
    Tendsto (fun j => traceTwoNorm τ (x j - a)) l (𝓝 0) := by
…

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

theorem OAI.KadisonKastler.FiniteVectorTrace.bounded_complete line 57

Source documentation

A uniformly bounded tracial two-Cauchy sequence has an actual limit in the concrete von Neumann algebra, with strong and two-norm convergence.

theorem FiniteVectorTrace.bounded_complete
    {τ : FaithfulTracialState (Algebra M)} (hτ : FiniteVectorTrace τ)
    (x : ℕ → Algebra M) {C : ℝ} (hC : 0 ≤ C) (hx : ∀ j, ‖x j‖ ≤ C)
    (hCauchy : ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N,
      traceTwoNorm τ (x m - x n) < ε) :
    ∃ a : Algebra M, ‖a‖ ≤ C ∧
      (∀ ξ, Tendsto (fun j => (x j : H →L[ℂ] H) ξ) atTop
        (𝓝 ((a : H →L[ℂ] H) ξ))) ∧
      Tendsto (fun j => traceTwoNorm τ (x j - a)) atTop (𝓝 0) := by
…

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