OAI/Analysis/JiangSu/MatrixAlgebras/MatrixPackingCornerRound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectPacking.exists_packing_step_with_corner line 15
  2. lemma OAI.DirectPacking.exists_precise_corner_round line 54
  3. structure OAI.DirectPacking.MatrixPackingCertificate line 119
  4. def OAI.DirectPacking.MatrixPackingCertificate.gap line 132
  5. def OAI.DirectPacking.MatrixPackingCertificate.energy line 133
  6. lemma OAI.DirectPacking.MatrixPackingCertificate.piece_le line 136
  7. def OAI.DirectPacking.MatrixPackingCertificate.zero line 139
  8. def OAI.DirectPacking.MatrixPackingCertificate.rebase line 148
  9. def OAI.DirectPacking.MatrixPackingCertificate.append line 152
  10. lemma OAI.DirectPacking.MatrixPackingCertificate.append_gap line 186
  11. lemma OAI.DirectPacking.MatrixPackingCertificate.append_energy line 194