OAI/Analysis/Commutator/UnitarySequence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.TracialSequence.boundedUnitary line 31
  2. lemma OAI.Kadison.TracialSequence.boundedUnitary_apply line 38
  3. def OAI.Kadison.TracialSequence.evalSequence line 41
  4. lemma OAI.Kadison.TracialSequence.eval_partialUnitary line 50
  5. lemma OAI.Kadison.TracialSequence.eval_power line 54
  6. lemma OAI.Kadison.TracialSequence.eval_word line 60
  7. def OAI.Kadison.TracialSequence.sequenceUnitary line 68
  8. lemma OAI.Kadison.TracialSequence.sequence_partial_map line 73
  9. lemma OAI.Kadison.TracialSequence.trace_left_zero_of_tendsto line 82
  10. lemma OAI.Kadison.TracialSequence.sequence_power_map line 89
  11. lemma OAI.Kadison.TracialSequence.sequence_word_map line 108
  12. lemma OAI.Kadison.TracialSequence.trace_sequence_power line 141
  13. lemma OAI.Kadison.TracialSequence.trace_sequence_word line 154