OAI/Analysis/JiangSu/Comparison/LocalizedCompression.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectComparison.cornerCFC_mem line 15
  2. lemma OAI.DirectComparison.cornerCFC_nonneg line 19
  3. lemma OAI.DirectComparison.cornerCFC_norm_le_one line 41
  4. lemma OAI.DirectComparison.localized_cutoff_mem line 53
  5. lemma OAI.DirectComparison.localized_cutoff_compression line 67
  6. lemma OAI.DirectComparison.positiveCut_trace_lower line 126
  7. structure OAI.DirectComparison.ProjectionPacking line 153
  8. def OAI.DirectComparison.ProjectionPacking.total line 165
  9. def OAI.DirectComparison.ProjectionPacking.residual line 166
  10. lemma OAI.DirectComparison.ProjectionPacking.total_projection line 168
  11. lemma OAI.DirectComparison.ProjectionPacking.total_le line 172
  12. lemma OAI.DirectComparison.ProjectionPacking.piece_le_total line 173
  13. lemma OAI.DirectComparison.ProjectionPacking.piece_le line 175
  14. lemma OAI.DirectComparison.ProjectionPacking.residual_projection line 176
  15. lemma OAI.DirectComparison.ProjectionPacking.residual_le line 178
  16. lemma OAI.DirectComparison.ProjectionPacking.total_add_residual line 180
  17. lemma OAI.DirectComparison.ProjectionPacking.piece_mul_residual line 181
  18. lemma OAI.DirectComparison.ProjectionPacking.residual_mul_piece line 185
  19. def OAI.DirectComparison.ProjectionPacking.empty line 191
  20. lemma OAI.DirectComparison.ProjectionPacking.empty_total line 198
  21. lemma OAI.DirectComparison.ProjectionPacking.empty_residual line 201
  22. def OAI.DirectComparison.ProjectionPacking.singleton line 204
  23. lemma OAI.DirectComparison.ProjectionPacking.singleton_total line 211
  24. def OAI.DirectComparison.ProjectionPacking.append line 216
  25. lemma OAI.DirectComparison.ProjectionPacking.append_total line 244
  26. lemma OAI.DirectComparison.ProjectionPacking.append_residual line 247
  27. lemma OAI.DirectComparison.ProjectionPacking.residual_append_le line 251
  28. lemma OAI.DirectComparison.ProjectionPacking.total_le_append line 254
  29. def OAI.DirectComparison.ProjectionPacking.refine line 258
  30. lemma OAI.DirectComparison.ProjectionPacking.refine_total line 274
  31. lemma OAI.DirectComparison.ProjectionPacking.refine_residual line 276