OAI/Combinatorics/MatchingCount/Sampling/Endpoints2.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.vertex_bound_of_perfect line 8
  2. lemma OAI.MatchingFPRAS.zero_of_vertex_bound line 25
  3. lemma OAI.MatchingFPRAS.even_of_perfect line 32
  4. lemma OAI.MatchingFPRAS.zero_of_not_even line 39
  5. lemma OAI.MatchingFPRAS.count_empty_graph line 44
  6. lemma OAI.MatchingFPRAS.edgeCard_le_input_length line 60
  7. lemma OAI.MatchingFPRAS.positive_vertex_input_bound line 77
  8. abbrev OAI.MatchingFPRAS.ExecutableInput.SparseInput line 86
  9. def OAI.MatchingFPRAS.ExecutableInput.sparseRep line 87
  10. def OAI.MatchingFPRAS.ExecutableInput.tooSparse line 89
  11. def OAI.MatchingFPRAS.ExecutableInput.tooSparseRealizer line 90
  12. lemma OAI.MatchingFPRAS.ExecutableInput.polynomial_tooSparse line 95
  13. lemma OAI.MatchingFPRAS.ExecutableInput.tooSparse_source line 100
  14. lemma OAI.MatchingFPRAS.ExecutableInput.tooSparse_zero line 102
  15. lemma OAI.MatchingFPRAS.ExecutableInput.tooSparse_false_bound line 105
  16. lemma OAI.MatchingFPRAS.ExecutableInput.tooSparse_false_input_bound line 110
  17. theorem OAI.MatchingFPRAS.ExecutableInput.tooSparse_post line 116