OAI/Analysis/KadisonKastler/TraceLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Limits in the faithful tracial two-norm

  1. theorem OAI.KadisonKastler.traceTwoNorm_zero line 17
  2. theorem OAI.KadisonKastler.traceTwoNorm_eq_zero_iff line 21
  3. theorem OAI.KadisonKastler.traceTwoNorm_limit_unique line 35

    Source documentation

    Limits in the faithful tracial two-norm are unique.

    theorem traceTwoNorm_limit_unique (Ļ„ : FaithfulTracialState B)
    {J : Type*} {l : Filter J} [l.NeBot] (x : J ā†’ B) {a b : B}
    (ha : Tendsto (fun j => traceTwoNorm Ļ„ (x j - a)) l (š“ 0))
    (hb : Tendsto (fun j => traceTwoNorm Ļ„ (x j - b)) l (š“ 0)) : a = b := by
ā€¦

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

  4. theorem OAI.KadisonKastler.traceTwoNorm_tendsto_mul line 50

    Source documentation

    Multiplication preserves two-norm limits on a uniformly bounded left factor.

    theorem traceTwoNorm_tendsto_mul (Ļ„ : FaithfulTracialState B)
    {J : Type*} {l : Filter J} (x y : J ā†’ B) (a b : B)
    {C : ā„} (hx : āˆ€ j, ā€–x jā€– ā‰¤ C)
    (ha : Tendsto (fun j => traceTwoNorm Ļ„ (x j - a)) l (š“ 0))
    (hb : Tendsto (fun j => traceTwoNorm Ļ„ (y j - b)) l (š“ 0)) :
    Tendsto (fun j => traceTwoNorm Ļ„ (x j * y j - a * b)) l (š“ 0) := by
ā€¦

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