OAI/Analysis/Pureness/Stabilization/ProductCuts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzTrace.abs_mul_left_cuntzBelow line 10
  2. lemma OAI.CuntzTrace.abs_star_cuntzBelow line 21
  3. lemma OAI.CuntzTrace.abs_mul_right_cuntzBelow line 26
  4. theorem OAI.CuntzTrace.product_cut_comparisons line 31
  5. theorem OAI.CuntzTrace.perturbation_cut_comparison line 58
  6. theorem OAI.CuntzTrace.product_cut_ranks line 71
  7. theorem OAI.CuntzTrace.adjoint_cut_comparison line 78
  8. theorem OAI.CuntzTrace.adjoint_cut_ranks line 91