OAI/Combinatorics/MatchingCount/Algorithm/Algorithm.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.LiteralAlgorithm.empty line 13
  2. def OAI.MatchingFPRAS.LiteralAlgorithm.emptyRealizer line 14
  3. lemma OAI.MatchingFPRAS.LiteralAlgorithm.polynomial_empty line 15
  4. def OAI.MatchingFPRAS.LiteralAlgorithm.invalid line 18
  5. def OAI.MatchingFPRAS.LiteralAlgorithm.invalidRealizer line 19
  6. lemma OAI.MatchingFPRAS.LiteralAlgorithm.polynomial_invalid line 25
  7. def OAI.MatchingFPRAS.LiteralAlgorithm.materialize line 32
  8. def OAI.MatchingFPRAS.LiteralAlgorithm.materializeRealizer line 33
  9. lemma OAI.MatchingFPRAS.LiteralAlgorithm.work_materialize line 35
  10. def OAI.MatchingFPRAS.LiteralAlgorithm.compute line 44
  11. def OAI.MatchingFPRAS.LiteralAlgorithm.computeRealizer line 46
  12. def OAI.MatchingFPRAS.LiteralAlgorithm.count line 50
  13. def OAI.MatchingFPRAS.LiteralAlgorithm.countRealizer line 52
  14. def OAI.MatchingFPRAS.LiteralAlgorithm.algorithm line 56
  15. def OAI.MatchingFPRAS.LiteralAlgorithm.algorithmRealizer line 58
  16. lemma OAI.MatchingFPRAS.LiteralAlgorithm.edgeNumbers_length line 63
  17. lemma OAI.MatchingFPRAS.LiteralAlgorithm.edgeNumbers_mem line 65
  18. def OAI.MatchingFPRAS.LiteralAlgorithm.reorder line 75
  19. lemma OAI.MatchingFPRAS.LiteralAlgorithm.reorder_mem line 77
  20. lemma OAI.MatchingFPRAS.LiteralAlgorithm.materialize_source line 84
  21. lemma OAI.MatchingFPRAS.LiteralAlgorithm.compute_mean line 91