OAI/Combinatorics/MatchingCount/Sampling/AssignmentEquiv.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.UnitRefresh.assignmentEquiv line 13
  2. lemma OAI.MatchingFPRAS.UnitRefresh.fiberCount_equiv line 23
  3. lemma OAI.MatchingFPRAS.UnitRefresh.assignmentPartition_equiv line 29
  4. abbrev OAI.MatchingFPRAS.UnitRefresh.Private line 43
  5. abbrev OAI.MatchingFPRAS.UnitRefresh.Shared line 45
  6. abbrev OAI.MatchingFPRAS.UnitRefresh.Outside line 47
  7. def OAI.MatchingFPRAS.UnitRefresh.splitLeaf line 49
  8. def OAI.MatchingFPRAS.UnitRefresh.LeafAt line 62
  9. lemma OAI.MatchingFPRAS.UnitRefresh.splitLeaf_bags line 66
  10. theorem OAI.MatchingFPRAS.UnitRefresh.tree_leaf_elimination line 77
  11. def OAI.MatchingFPRAS.UnitRefresh.rootBags line 86
  12. def OAI.MatchingFPRAS.UnitRefresh.rootAssignmentEquiv line 89
  13. def OAI.MatchingFPRAS.UnitRefresh.rootUpdate line 106
  14. lemma OAI.MatchingFPRAS.UnitRefresh.root_elimination line 109
  15. def OAI.MatchingFPRAS.UnitRefresh.splitRoot line 139
  16. theorem OAI.MatchingFPRAS.UnitRefresh.tree_root_elimination line 146
  17. def OAI.MatchingFPRAS.UnitRefresh.activePartition line 165
  18. def OAI.MatchingFPRAS.UnitRefresh.trim line 168
  19. def OAI.MatchingFPRAS.UnitRefresh.privateCount line 170
  20. def OAI.MatchingFPRAS.UnitRefresh.sharedCount line 173
  21. def OAI.MatchingFPRAS.UnitRefresh.activeFilterEquiv line 176
  22. lemma OAI.MatchingFPRAS.UnitRefresh.active_card_filter line 184
  23. lemma OAI.MatchingFPRAS.UnitRefresh.active_outside line 190
  24. theorem OAI.MatchingFPRAS.UnitRefresh.active_leaf_elimination line 200
  25. lemma OAI.MatchingFPRAS.UnitRefresh.active_root_elimination line 212
  26. lemma OAI.MatchingFPRAS.UnitRefresh.partition_isEmpty line 220
  27. lemma OAI.MatchingFPRAS.UnitRefresh.active_empty line 229
  28. def OAI.MatchingFPRAS.UnitRefresh.RankedBags line 232
  29. def OAI.MatchingFPRAS.UnitRefresh.advanceTable line 236
  30. def OAI.MatchingFPRAS.UnitRefresh.tableDP line 242
  31. def OAI.MatchingFPRAS.UnitRefresh.LegalPlan line 247
  32. theorem OAI.MatchingFPRAS.UnitRefresh.tableDP_correct line 255
  33. theorem OAI.MatchingFPRAS.UnitRefresh.rank_order_legal line 279