OAI/Combinatorics/MatchingCount/Sampling/Component.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.MatchingFPRAS.Transport.Sparse.decideOverlay line 15
  2. def OAI.MatchingFPRAS.Transport.Sparse.component line 21
  3. lemma OAI.MatchingFPRAS.Transport.Sparse.component_eq line 24
  4. def OAI.MatchingFPRAS.Transport.Sparse.allComponents line 29
  5. lemma OAI.MatchingFPRAS.Transport.Sparse.allComponents_eq line 31
  6. def OAI.MatchingFPRAS.Transport.Sparse.discrepancies line 36
  7. lemma OAI.MatchingFPRAS.Transport.Sparse.discrepancies_eq line 39
  8. def OAI.MatchingFPRAS.Transport.Sparse.cycle line 44
  9. lemma OAI.MatchingFPRAS.Transport.Sparse.cycle_eq line 53
  10. lemma OAI.MatchingFPRAS.Transport.Sparse.discrepancies_card line 58
  11. structure OAI.MatchingFPRAS.WeightedOptions line 69
  12. def OAI.MatchingFPRAS.WeightedOptions.pure line 82
  13. def OAI.MatchingFPRAS.WeightedOptions.map line 89
  14. def OAI.MatchingFPRAS.WeightedOptions.mix line 96
  15. def OAI.MatchingFPRAS.WeightedOptions.law line 113
  16. lemma OAI.MatchingFPRAS.WeightedOptions.law_nonneg line 115
  17. lemma OAI.MatchingFPRAS.WeightedOptions.law_sum line 120
  18. lemma OAI.MatchingFPRAS.WeightedOptions.pure_law line 125
  19. lemma OAI.MatchingFPRAS.WeightedOptions.mix_law line 129
  20. lemma OAI.MatchingFPRAS.WeightedOptions.sum_law_mul line 137
  21. lemma OAI.MatchingFPRAS.WeightedOptions.map_law line 146
  22. lemma OAI.MatchingFPRAS.WeightedOptions.map_first_law line 156
  23. def OAI.MatchingFPRAS.WeightedOptions.accept line 165
  24. lemma OAI.MatchingFPRAS.WeightedOptions.accept_law line 181
  25. def OAI.MatchingFPRAS.WeightedOptions.numbering line 201
  26. def OAI.MatchingFPRAS.WeightedOptions.uniform line 203
  27. lemma OAI.MatchingFPRAS.WeightedOptions.uniform_law line 212
  28. def OAI.MatchingFPRAS.WeightedOptions.neighbors line 220
  29. lemma OAI.MatchingFPRAS.WeightedOptions.neighbors_law line 238
  30. lemma OAI.MatchingFPRAS.Transport.Sparse.erased_eq line 260
  31. lemma OAI.MatchingFPRAS.Transport.Sparse.neighbors_real line 266
  32. lemma OAI.MatchingFPRAS.Transport.Sparse.color_degree line 290
  33. lemma OAI.MatchingFPRAS.Transport.Sparse.switch_degree line 295
  34. def OAI.MatchingFPRAS.Transport.Sparse.colorTable line 303
  35. def OAI.MatchingFPRAS.Transport.Sparse.switchTable line 309
  36. lemma OAI.MatchingFPRAS.Transport.Sparse.colorTable_law line 315
  37. lemma OAI.MatchingFPRAS.Transport.Sparse.switchTable_law line 322
  38. def OAI.MatchingFPRAS.Transport.Sparse.cycleTable line 330
  39. lemma OAI.MatchingFPRAS.Transport.Sparse.cycleTable_law line 336
  40. def OAI.MatchingFPRAS.Transport.Sparse.pairTable line 352
  41. lemma OAI.MatchingFPRAS.Transport.Sparse.pairTable_law line 362
  42. lemma OAI.MatchingFPRAS.Transport.Sparse.pairTable_size line 380