OAI/Combinatorics/MatchingCount/Algorithm/AlgorithmLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.PhysicalStream.qaverage_mono line 8
  2. lemma OAI.MatchingFPRAS.PhysicalStream.qaverage_indicator line 11
  3. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.mean_mono line 15
  4. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.mean_const line 20
  5. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.mean_indicator_eq_one line 25
  6. lemma OAI.MatchingFPRAS.LiteralAlgorithm.empty_source line 38
  7. lemma OAI.MatchingFPRAS.LiteralAlgorithm.invalid_source line 40
  8. lemma OAI.MatchingFPRAS.LiteralAlgorithm.invalid_zero line 44
  9. lemma OAI.MatchingFPRAS.LiteralAlgorithm.valid_even line 51
  10. lemma OAI.MatchingFPRAS.LiteralAlgorithm.valid_size line 56
  11. lemma OAI.MatchingFPRAS.LiteralAlgorithm.valid_two line 63
  12. def OAI.MatchingFPRAS.LiteralAlgorithm.Proper line 69
  13. def OAI.MatchingFPRAS.LiteralAlgorithm.AccurateWord line 71
  14. lemma OAI.MatchingFPRAS.LiteralAlgorithm.algorithm_proper line 73
  15. lemma OAI.MatchingFPRAS.LiteralAlgorithm.accurate_zero line 103
  16. lemma OAI.MatchingFPRAS.LiteralAlgorithm.proper_accurate_zero line 105
  17. lemma OAI.MatchingFPRAS.LiteralAlgorithm.algorithm_success line 111