OAI/Combinatorics/MatchingCount/Graphs/RemainingBags.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.UnitRefresh.Materialized.remainingBags line 13
  2. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.remainingRanked line 17
  3. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.remainingNonempty line 23
  4. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.remainingCard line 27
  5. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.remainingPositive line 36
  6. def OAI.MatchingFPRAS.UnitRefresh.Materialized.assembleEdge line 45
  7. def OAI.MatchingFPRAS.UnitRefresh.Materialized.residualSampler line 49
  8. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.sampleUnit_step line 57
  9. def OAI.MatchingFPRAS.UnitRefresh.Materialized.renumberedSplitEquiv line 66
  10. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.renumberedSplitEquiv_apply line 76
  11. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.sampleUnit_step_law line 82
  12. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.exact_unit_step line 91
  13. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.residualSampler_law line 112
  14. theorem OAI.MatchingFPRAS.UnitRefresh.Materialized.sampleUnit_tv line 122
  15. instance OAI.MatchingFPRAS.UnitRefresh.Computable.edgeDec line 185
  16. instance OAI.MatchingFPRAS.UnitRefresh.Computable.allowedDec line 188
  17. def OAI.MatchingFPRAS.UnitRefresh.Computable.edge line 191
  18. lemma OAI.MatchingFPRAS.UnitRefresh.Computable.edge_spec line 195
  19. lemma OAI.MatchingFPRAS.UnitRefresh.Computable.edge_eq line 199
  20. def OAI.MatchingFPRAS.UnitRefresh.Computable.mate line 202
  21. lemma OAI.MatchingFPRAS.UnitRefresh.Computable.mate_eq line 205
  22. def OAI.MatchingFPRAS.UnitRefresh.Computable.fromMatching line 210
  23. lemma OAI.MatchingFPRAS.UnitRefresh.Computable.from_eq line 219
  24. def OAI.MatchingFPRAS.UnitRefresh.Computable.toMatching line 224
  25. lemma OAI.MatchingFPRAS.UnitRefresh.Computable.to_eq line 228
  26. def OAI.MatchingFPRAS.UnitRefresh.Computable.pairingEquiv line 230
  27. def OAI.MatchingFPRAS.UnitRefresh.orderedEnum line 246
  28. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.colorEquiv line 252
  29. def OAI.MatchingFPRAS.UnitRefresh.numberedBags line 279
  30. lemma OAI.MatchingFPRAS.UnitRefresh.mem_numberedBags line 282
  31. def OAI.MatchingFPRAS.UnitRefresh.numberedRank line 286
  32. def OAI.MatchingFPRAS.UnitRefresh.numberedParent line 288
  33. lemma OAI.MatchingFPRAS.UnitRefresh.numberedParent_iff line 291
  34. lemma OAI.MatchingFPRAS.UnitRefresh.numberedRanked line 295
  35. lemma OAI.MatchingFPRAS.UnitRefresh.numberedNonempty line 305
  36. lemma OAI.MatchingFPRAS.UnitRefresh.numberedDecreasing line 308
  37. def OAI.MatchingFPRAS.UnitRefresh.numberingEquiv line 313
  38. lemma OAI.MatchingFPRAS.UnitRefresh.numbered_count_pos line 318
  39. def OAI.MatchingFPRAS.UnitRefresh.sampleNumbered line 327
  40. theorem OAI.MatchingFPRAS.UnitRefresh.sampleNumbered_tv line 336
  41. def OAI.MatchingFPRAS.UnitRefresh.sampleMatching line 351
  42. theorem OAI.MatchingFPRAS.UnitRefresh.sampleMatching_tv line 359