OAI/Combinatorics/MatchingCount/Graphs/Admissible.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Variation.bind_perturbation_on line 13
  2. theorem OAI.MatchingFPRAS.WeightedOptions.drawThen_tv_on line 46
  3. def OAI.MatchingFPRAS.Replica.admissible line 71
  4. lemma OAI.MatchingFPRAS.Replica.scanChoice_support line 76
  5. lemma OAI.MatchingFPRAS.Replica.localSampler_tv_on line 93
  6. theorem OAI.MatchingFPRAS.Replica.sampleScan_tv_on line 137
  7. lemma OAI.MatchingFPRAS.Replica.metropolis_normalize line 163
  8. def OAI.MatchingFPRAS.Transport.Sparse.rationalWeight line 186
  9. lemma OAI.MatchingFPRAS.Transport.Sparse.rationalWeight_pos line 189
  10. lemma OAI.MatchingFPRAS.Transport.Sparse.rationalWeight_cast line 194
  11. def OAI.MatchingFPRAS.Transport.Sparse.rationalPairWeight line 199
  12. lemma OAI.MatchingFPRAS.Transport.Sparse.rationalPairWeight_pos line 202
  13. def OAI.MatchingFPRAS.Transport.Sparse.pairStepTable line 206
  14. theorem OAI.MatchingFPRAS.Transport.Sparse.pairStepTable_law line 213
  15. theorem OAI.MatchingFPRAS.Transport.Sparse.pairStepTable_tv line 233
  16. lemma OAI.MatchingFPRAS.FiniteChoice.choose_pos line 258
  17. lemma OAI.MatchingFPRAS.FiniteChoice.chooseBits_pos line 265
  18. instance OAI.MatchingFPRAS.UnitRefresh.(instance at line 273) line 273
  19. instance OAI.MatchingFPRAS.UnitRefresh.(instance at line 280) line 280
  20. def OAI.MatchingFPRAS.UnitRefresh.completionSum line 292
  21. lemma OAI.MatchingFPRAS.UnitRefresh.completion_monomial line 297
  22. def OAI.MatchingFPRAS.UnitRefresh.interfacePolynomial line 302
  23. def OAI.MatchingFPRAS.UnitRefresh.convolution line 307
  24. lemma OAI.MatchingFPRAS.UnitRefresh.prod_monomials line 311
  25. theorem OAI.MatchingFPRAS.UnitRefresh.convolution_recurrence line 317
  26. lemma OAI.MatchingFPRAS.UnitRefresh.interface_natDegree line 332
  27. lemma OAI.MatchingFPRAS.UnitRefresh.convolution_natDegree line 341
  28. theorem OAI.MatchingFPRAS.UnitRefresh.convolution_finite_evaluation line 347
  29. def OAI.MatchingFPRAS.UnitRefresh.Pairing.sigma line 363
  30. structure OAI.MatchingFPRAS.UnitRefresh.ColoredPairing line 374
  31. lemma OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.ext line 381
  32. instance OAI.MatchingFPRAS.UnitRefresh.(instance at line 385) line 385
  33. instance OAI.MatchingFPRAS.UnitRefresh.(instance at line 390) line 390
  34. abbrev OAI.MatchingFPRAS.UnitRefresh.Assignment line 392
  35. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.fiber line 394
  36. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.glue line 400
  37. def OAI.MatchingFPRAS.UnitRefresh.assignmentPairingEquiv line 407
  38. theorem OAI.MatchingFPRAS.UnitRefresh.coloredPairing_card line 429