OAI/Combinatorics/MatchingPSD/SequentialTests.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PerfectMatchingPSD.congruence_mono line 13
  2. lemma OAI.PerfectMatchingPSD.effect_le_one line 20
  3. lemma OAI.PerfectMatchingPSD.effects_square_sum_le line 26
  4. def OAI.PerfectMatchingPSD.sequentialProduct line 35
  5. lemma OAI.PerfectMatchingPSD.sum_function_succ line 40
  6. lemma OAI.PerfectMatchingPSD.sequentialProduct_sum_le line 47
  7. lemma OAI.PerfectMatchingPSD.sequentialProduct_error line 62
  8. lemma OAI.PerfectMatchingPSD.norm_sqrt_trace_one line 85
  9. lemma OAI.PerfectMatchingPSD.norm_mul_sqrt_sq line 93
  10. lemma OAI.PerfectMatchingPSD.norm_mul_sq_lower line 103
  11. lemma OAI.PerfectMatchingPSD.trace_product_upper line 111
  12. lemma OAI.PerfectMatchingPSD.sequentialProduct_trace_lower line 121
  13. lemma OAI.PerfectMatchingPSD.nearly_perfect_bit_tests line 139