OAI/Analysis/JiangSu/Excision/ExcisionUpperCut.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectComparison.upperCut line 16
  2. lemma OAI.DirectComparison.upperCut_cfc line 19
  3. lemma OAI.DirectComparison.upperCut_nonneg line 24
  4. lemma OAI.DirectComparison.upperCut_le_one line 27
  5. lemma OAI.DirectComparison.upperCut_norm_le line 37
  6. lemma OAI.DirectComparison.upperCut_support_error line 42
  7. lemma OAI.DirectComparison.upperCut_trace_lower line 69
  8. lemma OAI.DirectComparison.trace_positive_sandwich_le line 111
  9. lemma OAI.DirectComparison.trace_sub_real_le_norm line 133
  10. lemma OAI.DirectComparison.compression_swap_error line 139
  11. theorem OAI.DirectComparison.trace_full_frame_compression line 148
  12. def OAI.DirectComparison.hereditaryUpperCut line 176
  13. lemma OAI.DirectComparison.hereditaryUpperCut_nonneg line 178
  14. lemma OAI.DirectComparison.norm_contractive_sandwich line 183
  15. lemma OAI.DirectComparison.hereditaryUpperCut_norm_le line 191
  16. lemma OAI.DirectComparison.hereditaryUpperCut_support line 196
  17. lemma OAI.DirectComparison.hereditaryUpperCut_error line 201
  18. lemma OAI.DirectComparison.hereditaryUpperCut_trace line 219
  19. theorem OAI.DirectComparison.hereditaryUpperCut_trace_lower line 232