OAI/Combinatorics/MatchingCount/Sampling/Sym2Order.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.sym2Order line 12
  2. def OAI.MatchingFPRAS.Transport.bagEdgeOrder line 18
  3. def OAI.MatchingFPRAS.Transport.rationalTierBase line 24
  4. lemma OAI.MatchingFPRAS.Transport.rationalTierBase_cast line 27
  5. def OAI.MatchingFPRAS.Transport.rationalSlotWeight line 30
  6. lemma OAI.MatchingFPRAS.Transport.rationalSlotWeight_cast line 35
  7. lemma OAI.MatchingFPRAS.Transport.rationalSlotWeight_pos line 41
  8. def OAI.MatchingFPRAS.Transport.bagEdgeFintype line 53
  9. abbrev OAI.MatchingFPRAS.Transport.BagPM line 57
  10. lemma OAI.MatchingFPRAS.Transport.parallels_bound line 62
  11. def OAI.MatchingFPRAS.Transport.sampleLadderPair line 71
  12. lemma OAI.MatchingFPRAS.Transport.pairProposal_instances line 78
  13. lemma OAI.MatchingFPRAS.Transport.pairLaw_instances line 89
  14. lemma OAI.MatchingFPRAS.Transport.pairProposal_eq line 94
  15. lemma OAI.MatchingFPRAS.Transport.pairLaw_eq line 103
  16. lemma OAI.MatchingFPRAS.Transport.metropolis_eq_capacity line 113
  17. lemma OAI.MatchingFPRAS.Transport.sampleLadderPair_tv line 124
  18. lemma OAI.MatchingFPRAS.Variation.imageLaw_ignoreRight line 157
  19. lemma OAI.MatchingFPRAS.Transport.gibbs_one_uniform line 176
  20. lemma OAI.MatchingFPRAS.Transport.base_slotLaw line 182
  21. def OAI.MatchingFPRAS.Transport.prodOrder line 208
  22. def OAI.MatchingFPRAS.Transport.sumOrder line 211
  23. abbrev OAI.MatchingFPRAS.Transport.LocalBits line 224
  24. abbrev OAI.MatchingFPRAS.Transport.ScanBits line 227
  25. def OAI.MatchingFPRAS.Transport.pairDraw line 229
  26. def OAI.MatchingFPRAS.Transport.baseDraw line 233
  27. def OAI.MatchingFPRAS.Transport.ladderScan line 236
  28. def OAI.MatchingFPRAS.Transport.scanErrorNumerator line 241
  29. lemma OAI.MatchingFPRAS.Transport.ladderScan_tv line 247
  30. def OAI.MatchingFPRAS.Transport.ladderRun line 289
  31. lemma OAI.MatchingFPRAS.Transport.ladderKernel_nonneg line 293
  32. lemma OAI.MatchingFPRAS.Transport.ladderKernel_sum line 300
  33. lemma OAI.MatchingFPRAS.Transport.ladderRun_walk_tv line 312
  34. lemma OAI.MatchingFPRAS.Transport.ladderRun_gibbs_tv line 325
  35. def OAI.MatchingFPRAS.Transport.bitPrecision line 348
  36. lemma OAI.MatchingFPRAS.Transport.bitPrecision_error line 350
  37. def OAI.MatchingFPRAS.Transport.pairBitsEquiv line 363
  38. def OAI.MatchingFPRAS.Transport.matrixBitsEquiv line 367
  39. def OAI.MatchingFPRAS.Transport.scanBitCount line 370
  40. def OAI.MatchingFPRAS.Transport.scanBitsEquiv line 372
  41. def OAI.MatchingFPRAS.Transport.runBitsEquiv line 378
  42. def OAI.MatchingFPRAS.Transport.ladderBitRun line 400
  43. lemma OAI.MatchingFPRAS.Transport.ladderBitRun_walk_tv line 405