OAI/Analysis/JiangSu/MatrixAlgebras/MatrixSmallPacking.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectPacking.exists_small_matrix_packing line 15
  2. lemma OAI.DirectPacking.orthogonal_sum_star_mul line 56
  3. lemma OAI.DirectPacking.orthogonal_sum_twoNorm_sq line 65
  4. lemma OAI.DirectPacking.supported_orthogonal line 71
  5. lemma OAI.DirectPacking.twoNorm_compress_le line 81
  6. lemma OAI.DirectPacking.supported_sum_norm_le_one line 89
  7. def OAI.DirectPacking.MatrixPackingCertificate.compress line 117
  8. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_star line 121
  9. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_add line 126
  10. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_smul line 130
  11. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_norm_le_one line 134
  12. lemma OAI.DirectPacking.twoNorm_mul_left_contraction line 155
  13. lemma OAI.DirectPacking.twoNorm_mul_right_contraction line 158
  14. lemma OAI.DirectPacking.norm_mul_contractions line 162
  15. lemma OAI.DirectPacking.orthogonal_sum_mul line 166
  16. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_left line 186
  17. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_right line 190
  18. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_unit_gap line 194
  19. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_mul_gap line 211