OAI/Analysis/JiangSu/TraceCone/RankCyclic.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TraceCone.supported_cfc_factor line 16
  2. lemma OAI.TraceCone.ExtendedTrace.tracial_supported_cfc line 36
  3. lemma OAI.TraceCone.ExtendedTrace.tracial_power_cut line 72
  4. lemma OAI.TraceCone.ExtendedTrace.tracial_power_le line 93
  5. theorem OAI.TraceCone.ExtendedTrace.tracial_power line 108
  6. theorem OAI.TraceCone.ExtendedTrace.rank_tracial line 114
  7. def OAI.TraceCone.Positive.conjugate line 124
  8. lemma OAI.TraceCone.Positive.conjugate_eq_starMul line 127
  9. lemma OAI.TraceCone.Positive.mulStar_sqrt_mul_le line 136
  10. lemma OAI.TraceCone.ExtendedTrace.rank_conjugate_le line 152
  11. theorem OAI.TraceCone.ExtendedTrace.rank_le_of_cuntzBelow line 158
  12. theorem OAI.TraceCone.ExtendedTrace.rank_eq_of_cuntzEquivalent line 175
  13. lemma OAI.TraceCone.Positive.power_cut_le line 184
  14. theorem OAI.TraceCone.ExtendedTrace.rank_cut_le_trace line 223
  15. theorem OAI.TraceCone.ExtendedTrace.rank_eq_zero_iff line 241
  16. lemma OAI.TraceCone.Positive.cut_cut line 264
  17. theorem OAI.TraceCone.ExtendedTrace.trace_le_norm_mul_rank line 287
  18. theorem OAI.TraceCone.ExtendedTrace.controller_trace_bound line 310
  19. theorem OAI.TraceCone.ExtendedTrace.trace_cut_loss line 327