OAI/Combinatorics/MatchingCount/Sampling/RankOrder.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.UnitRefresh.rankOrder line 13
  2. lemma OAI.MatchingFPRAS.UnitRefresh.rankOrder_mem line 17
  3. lemma OAI.MatchingFPRAS.UnitRefresh.rankOrder_length line 23
  4. lemma OAI.MatchingFPRAS.UnitRefresh.rankOrder_sorted line 29
  5. lemma OAI.MatchingFPRAS.UnitRefresh.rankOrder_legal line 36
  6. lemma OAI.MatchingFPRAS.UnitRefresh.active_univ line 44
  7. theorem OAI.MatchingFPRAS.UnitRefresh.ranked_tableDP_correct line 55
  8. lemma OAI.MatchingFPRAS.UnitRefresh.private_le_card line 63
  9. lemma OAI.MatchingFPRAS.UnitRefresh.shared_le_card line 68
  10. lemma OAI.MatchingFPRAS.UnitRefresh.private_add_shared line 73
  11. lemma OAI.MatchingFPRAS.UnitRefresh.advanceTable_congr line 96
  12. def OAI.MatchingFPRAS.UnitRefresh.capTable line 124
  13. def OAI.MatchingFPRAS.UnitRefresh.finiteDP line 127
  14. lemma OAI.MatchingFPRAS.UnitRefresh.finiteDP_correct line 134
  15. theorem OAI.MatchingFPRAS.UnitRefresh.finite_ranked_count line 150
  16. abbrev OAI.MatchingFPRAS.UnitRefresh.withoutPair line 167
  17. abbrev OAI.MatchingFPRAS.UnitRefresh.residualBags line 169
  18. abbrev OAI.MatchingFPRAS.UnitRefresh.Partner line 172
  19. lemma OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.subtype_hext line 176
  20. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.remove line 193
  21. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.insert line 200
  22. lemma OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.insert_color line 224
  23. lemma OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.insert_color_residual line 230
  24. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.split line 237
  25. lemma OAI.MatchingFPRAS.UnitRefresh.partner_card line 272
  26. def OAI.MatchingFPRAS.UnitRefresh.residualCount line 276
  27. lemma OAI.MatchingFPRAS.UnitRefresh.residualCount_eq line 281
  28. theorem OAI.MatchingFPRAS.UnitRefresh.unit_self_reduction line 293
  29. abbrev OAI.MatchingFPRAS.UnitRefresh.Materialized.Table line 311
  30. def OAI.MatchingFPRAS.UnitRefresh.Materialized.read line 313
  31. def OAI.MatchingFPRAS.UnitRefresh.Materialized.tabulate line 315
  32. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.read_tabulate line 318
  33. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.tabulate_length line 328
  34. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.tabulate_rows line 331
  35. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.tabulate_cells line 336
  36. def OAI.MatchingFPRAS.UnitRefresh.Materialized.entry line 340
  37. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.entry_eq line 351
  38. def OAI.MatchingFPRAS.UnitRefresh.Materialized.update line 358
  39. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.read_update line 362
  40. def OAI.MatchingFPRAS.UnitRefresh.Materialized.run line 370
  41. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.read_run line 376
  42. def OAI.MatchingFPRAS.UnitRefresh.Materialized.initial line 388
  43. def OAI.MatchingFPRAS.UnitRefresh.Materialized.count line 390
  44. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.count_eq line 395
  45. def OAI.MatchingFPRAS.UnitRefresh.Materialized.cellsWritten line 411
  46. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.cellsWritten_bound line 416