OAI/Combinatorics/MatchingPSD/MatrixAverages.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PerfectMatchingPSD.matrix_expect_eq line 14
  2. lemma OAI.PerfectMatchingPSD.matrix_expect_apply line 20
  3. lemma OAI.PerfectMatchingPSD.matrix_expect_psd line 26
  4. lemma OAI.PerfectMatchingPSD.trace_mul_expect line 32
  5. lemma OAI.PerfectMatchingPSD.expect_abs_bound line 39
  6. def OAI.PerfectMatchingPSD.extensionMatrix line 55
  7. def OAI.PerfectMatchingPSD.cellMatrix line 60
  8. lemma OAI.PerfectMatchingPSD.cellMatrix_apply line 66
  9. lemma OAI.PerfectMatchingPSD.cellMatrix_psd line 76
  10. lemma OAI.PerfectMatchingPSD.cellMatrix_star line 86
  11. lemma OAI.PerfectMatchingPSD.trace_cellMatrix line 91
  12. lemma OAI.PerfectMatchingPSD.extensionAverage_sq_bound line 100