OAI/Analysis/TracialSplitting/FinitePacking.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentMain.PositiveDiagonal line 17
  2. lemma OAI.CurrentMain.traceTwoNorm_sub_swap line 29
  3. def OAI.CurrentMain.OrthogonalProjectionPair.zero line 37
  4. structure OAI.CurrentMain.PackingBounds line 46
  5. theorem OAI.CurrentMain.finite_packing_from_diagonals line 52
  6. lemma OAI.CurrentMain.exists_packing_parameters line 142
  7. lemma OAI.CurrentMain.OrthogonalProjectionPair.halving_le line 202
  8. theorem OAI.CurrentMain.finite_set_splitting_from_diagonals line 229
  9. abbrev OAI.CurrentMain.DiagonalTestSpace line 268
  10. def OAI.CurrentMain.diagonalTestPoint line 271
  11. def OAI.CurrentMain.diagonalTestAtom line 273
  12. def OAI.CurrentMain.diagonalTestAtoms line 277
  13. def OAI.CurrentMain.DiagonalDualBound line 280
  14. lemma OAI.CurrentMain.diagonalTestPoint_mem_closure line 284
  15. lemma OAI.CurrentMain.diagonalTest_sum line 295
  16. theorem OAI.CurrentMain.positiveDiagonal_of_dualBound line 303
  17. theorem OAI.CurrentMain.diagonal_separation_certificate line 342