OAI/Analysis/KadisonKastler/TracialSequenceQuotient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The faithful trace on the tracial sequence quotient

  1. abbrev OAI.KadisonKastler.TracialSequenceQuotient line 17
  2. instance OAI.KadisonKastler.tracialSequenceQuotientCStarAlgebra line 24
  3. def OAI.KadisonKastler.tracialSequenceQuotientMap line 27
  4. theorem OAI.KadisonKastler.tracialSequenceQuotientMap_surjective line 31
  5. theorem OAI.KadisonKastler.tracialSequenceQuotientMap_eq_zero_iff line 35
  6. def OAI.KadisonKastler.tracialQuotientLinear line 49
  7. theorem OAI.KadisonKastler.tracialQuotientLinear_map line 67
  8. def OAI.KadisonKastler.tracialQuotientTrace line 72

    Source documentation

    The quotient trace is faithful because exactly the two-null ideal was removed.

    def tracialQuotientTrace : FaithfulTracialState (TracialSequenceQuotient τ ω) where
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TracialSequenceQuotient

  9. instance OAI.KadisonKastler.tracialSequenceQuotientNontrivial line 94
  10. theorem OAI.KadisonKastler.tracialQuotientTrace_limit line 103

    Source documentation

    The constructed quotient has the required coordinate trace formula.

    theorem tracialQuotientTrace_limit (x : VaryingBoundedSequence B) :
    Tendsto (fun j => (τ j).toLinearMap (x j)) (ω : Filter ℕ)
      (𝓝 ((tracialQuotientTrace τ ω).toLinearMap (tracialSequenceQuotientMap τ ω x))) :=
…

    Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.tracialQuotientTrace, OAI.KadisonKastler.tracialSequenceQuotientMap

  11. theorem OAI.KadisonKastler.tracialQuotientTwoNorm_limit line 109

    Source documentation

    Coordinate two-norms converge to the quotient two-norm.

    theorem tracialQuotientTwoNorm_limit (x : VaryingBoundedSequence B) :
    Tendsto (fun j => traceTwoNorm (τ j) (x j)) (ω : Filter ℕ)
      (𝓝 (traceTwoNorm (tracialQuotientTrace τ ω) (tracialSequenceQuotientMap τ ω x))) := by
…

    Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.tracialQuotientTrace, OAI.KadisonKastler.tracialSequenceQuotientMap