OAI/Analysis/JiangSu/TraceCone/Weights.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TraceCone.Positive.sum line 17
  2. theorem OAI.TraceCone.ExtendedTrace.zero_apply line 24
  3. theorem OAI.TraceCone.ExtendedTrace.zero_of_le line 26
  4. theorem OAI.TraceCone.ExtendedTrace.map_sum line 30
  5. theorem OAI.TraceCone.ExtendedTrace.finite_positive_partition line 41
  6. def OAI.TraceCone.Positive.cut line 64
  7. theorem OAI.TraceCone.Positive.cut_le line 67
  8. theorem OAI.TraceCone.Positive.norm_sub_cut_le line 74
  9. theorem OAI.TraceCone.Positive.tendsto_cut line 91
  10. theorem OAI.TraceCone.ExtendedTrace.le_of_forall_cut_le line 104
  11. theorem OAI.TraceCone.ExtendedTrace.eq_iSup_cuts line 115
  12. def OAI.TraceCone.CanonicalConverges line 124
  13. theorem OAI.TraceCone.canonicalConverges_const line 130
  14. theorem OAI.TraceCone.canonicalConverges_const_iff line 136