OAI/Analysis/JiangSu/TraceCone/CuntzIdentities.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TraceCone.squareCutMultiplier line 13
  2. lemma OAI.TraceCone.squareCutMultiplier_continuous line 16
  3. lemma OAI.TraceCone.squareCutMultiplier_zero line 22
  4. lemma OAI.TraceCone.squareCutMultiplier_identity line 25
  5. theorem OAI.TraceCone.starMul_cut_factorization line 39
  6. theorem OAI.TraceCone.starMul_cuntzBelow_mulStar line 61
  7. theorem OAI.TraceCone.mulStar_cuntzBelow_starMul line 68
  8. theorem OAI.TraceCone.starMul_cuntzBelow_iff line 73
  9. lemma OAI.TraceCone.regularized_comparison line 83
  10. theorem OAI.TraceCone.CuntzBelow.of_le_smul line 131
  11. theorem OAI.TraceCone.CuntzBelow.of_le line 151
  12. theorem OAI.TraceCone.conjugate_cuntzBelow line 155
  13. theorem OAI.TraceCone.cut_cuntzBelow_of_norm_sub_lt line 160