OAI/Analysis/Pureness/Stabilization/AbsoluteComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.Positive.abs line 10
  2. lemma OAI.CuntzTrace.Positive.abs_sq line 11
  3. lemma OAI.CuntzTrace.squareCutMultiplier_bound line 15
  4. lemma OAI.CuntzTrace.squareCut_factorization line 29
  5. lemma OAI.CuntzTrace.abs_cuntzBelow_starMul line 49
  6. lemma OAI.CuntzTrace.starMul_cuntzBelow_abs line 56
  7. lemma OAI.CuntzTrace.starMul_add_le line 72
  8. theorem OAI.CuntzTrace.abs_cut_cuntzBelow_of_norm_sub_lt line 84