OAI/Analysis/JiangSu/TraceCone/Cuntz.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TraceCone.conjugate_norm_le line 15
  2. theorem OAI.TraceCone.CuntzBelow.zero line 27
  3. theorem OAI.TraceCone.CuntzBelow.refl line 31
  4. theorem OAI.TraceCone.CuntzBelow.eq_zero line 54
  5. theorem OAI.TraceCone.CuntzBelow.trans line 60
  6. theorem OAI.TraceCone.CuntzBelow.of_tendsto line 89
  7. theorem OAI.TraceCone.CuntzBelow.of_cuts line 102
  8. def OAI.TraceCone.cutMultiplier line 125
  9. lemma OAI.TraceCone.cutMultiplier_continuous line 127
  10. lemma OAI.TraceCone.cutMultiplier_zero line 132
  11. lemma OAI.TraceCone.cutMultiplier_sq line 135
  12. lemma OAI.TraceCone.cutMultiplier_identity line 139
  13. lemma OAI.TraceCone.cutMultiplier_bound line 151
  14. lemma OAI.TraceCone.fixedCut_factorization line 160
  15. theorem OAI.TraceCone.bounded_witness line 181
  16. theorem OAI.TraceCone.bounded_coordinate_witnesses line 217
  17. theorem OAI.TraceCone.cut_cuntzBelow line 237
  18. theorem OAI.TraceCone.cuntzBelow_iff_cuts line 243