OAI/Analysis/JiangSu/TraceCone/AbsoluteComparison.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TraceCone.Positive.abs line 15
  2. lemma OAI.TraceCone.Positive.abs_sq line 16
  3. lemma OAI.TraceCone.squareCutMultiplier_bound line 20
  4. lemma OAI.TraceCone.squareCut_factorization line 33
  5. lemma OAI.TraceCone.abs_cuntzBelow_starMul line 53
  6. lemma OAI.TraceCone.starMul_cuntzBelow_abs line 60
  7. lemma OAI.TraceCone.starMul_add_le line 76
  8. theorem OAI.TraceCone.abs_cut_cuntzBelow_of_norm_sub_lt line 88
  9. def OAI.TraceCone.truncationMultiplier line 156
  10. lemma OAI.TraceCone.truncationMultiplier_continuous line 157
  11. lemma OAI.TraceCone.truncationMultiplier_zero line 162
  12. lemma OAI.TraceCone.truncationMultiplier_identity line 163
  13. theorem OAI.TraceCone.exists_cut_truncation line 171