OAI/Combinatorics/MatchingCount/Graphs/CompleteGraph.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.completeGraph line 8
  2. def OAI.MatchingFPRAS.rawWeight line 18
  3. def OAI.MatchingFPRAS.rawPartition line 21
  4. lemma OAI.MatchingFPRAS.graph_edges_subset_complete line 26
  5. lemma OAI.MatchingFPRAS.mem_perfectMatchings line 31
  6. lemma OAI.MatchingFPRAS.pm_subset_complete line 36
  7. lemma OAI.MatchingFPRAS.rawWeight_nonneg line 42
  8. lemma OAI.MatchingFPRAS.rawWeight_one line 48
  9. lemma OAI.MatchingFPRAS.rawWeight_bad line 54
  10. theorem OAI.MatchingFPRAS.raw_padding_bound line 68
  11. theorem OAI.MatchingFPRAS.perfect_vertex_factor line 114
  12. def OAI.MatchingFPRAS.weightedPartition line 144
  13. theorem OAI.MatchingFPRAS.vertex_scaled_partition line 147
  14. def OAI.MatchingFPRAS.NearPerfect line 167
  15. def OAI.MatchingFPRAS.holePartition line 172
  16. def OAI.MatchingFPRAS.holeRatio line 177
  17. theorem OAI.MatchingFPRAS.near_vertex_factor line 183
  18. theorem OAI.MatchingFPRAS.hole_partition_vertex_scaling line 233
  19. theorem OAI.MatchingFPRAS.hole_ratio_vertex_scaling line 256
  20. def OAI.MatchingFPRAS.Counting.scheduleAdmissible line 276
  21. theorem OAI.MatchingFPRAS.Counting.counting_schedule_exists line 281