OAI/Analysis/JiangSu/TraceCone/ProductCuts.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TraceCone.abs_mul_left_cuntzBelow line 15
  2. lemma OAI.TraceCone.abs_star_cuntzBelow line 26
  3. lemma OAI.TraceCone.abs_mul_right_cuntzBelow line 31
  4. theorem OAI.TraceCone.product_cut_comparisons line 36
  5. theorem OAI.TraceCone.perturbation_cut_comparison line 65
  6. theorem OAI.TraceCone.product_cut_ranks line 75
  7. theorem OAI.TraceCone.adjoint_cut_comparison line 82
  8. theorem OAI.TraceCone.adjoint_cut_ranks line 95
  9. theorem OAI.TraceCone.ennreal_add_self_eq_iff line 109
  10. def OAI.TraceCone.idealIndicator line 119
  11. theorem OAI.TraceCone.idealIndicator_eq_zero line 122
  12. theorem OAI.TraceCone.idealIndicator_add_eq_iff line 127
  13. theorem OAI.TraceCone.idempotent_function_iff_indicator line 140
  14. theorem OAI.TraceCone.ExtendedTrace.isClosed_zeroSet line 157
  15. theorem OAI.TraceCone.ExtendedTrace.idempotent_iff_zero_or_top line 161
  16. theorem OAI.TraceCone.ExtendedTrace.idempotent_eq_indicator line 165
  17. theorem OAI.TraceCone.lowerSemicontinuous_idealIndicator line 180
  18. def OAI.TraceCone.zeroIdealWeight line 197
  19. theorem OAI.TraceCone.zeroIdealWeight_eq_zero line 224
  20. theorem OAI.TraceCone.zeroIdealWeight_lt_top line 228
  21. theorem OAI.TraceCone.zeroIdealWeight_detects line 234