OAI/Analysis/KadisonKastler/TracialSequenceIdeal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.TraceNullSequence line 18
2. theorem OAI.KadisonKastler.traceNullSequence_add line 22
3. theorem OAI.KadisonKastler.traceNullSequence_mul_left line 30
4. theorem OAI.KadisonKastler.traceNullSequence_mul_right line 40
5. theorem OAI.KadisonKastler.isClosed_traceNullSequence line 49
6. def OAI.KadisonKastler.traceNullClosedIdeal line 71
7. theorem OAI.KadisonKastler.tracialSequenceValue_eq_zero_of_null line 96

   Source documentation

   The canonical trace vanishes on the two-norm null ideal.

   theorem tracialSequenceValue_eq_zero_of_null {x : VaryingBoundedSequence B}
       (hx : TraceNullSequence τ ω x) : tracialSequenceValue τ ω x = 0 := by
   …

   Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.TraceNullSequence, OAI.KadisonKastler.tracialSequenceValue

8. theorem OAI.KadisonKastler.tracialSequenceValue_square_eq_zero_iff line 106

   Source documentation

   A square has zero limit trace precisely when its sequence is two-null.

   theorem tracialSequenceValue_square_eq_zero_iff (x : VaryingBoundedSequence B) :
       tracialSequenceValue τ ω (star x * x) = 0 ↔ TraceNullSequence τ ω x := by
   …

   Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.tracialSequenceValue, OAI.KadisonKastler.TraceNullSequence