OAI/Combinatorics/MatchingCount/Sampling/MetropolisChoice.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.WeightedOptions.metropolisChoice line 13
  2. lemma OAI.MatchingFPRAS.WeightedOptions.real_law_sum line 18
  3. lemma OAI.MatchingFPRAS.WeightedOptions.row_eq_of_off line 21
  4. lemma OAI.MatchingFPRAS.WeightedOptions.min_ratio line 34
  5. theorem OAI.MatchingFPRAS.WeightedOptions.metropolisChoice_law line 39
  6. lemma OAI.MatchingFPRAS.WeightedOptions.metropolisChoice_size line 55
  7. def OAI.MatchingFPRAS.Variation.uniform line 69
  8. lemma OAI.MatchingFPRAS.Variation.uniform_nonneg line 71
  9. lemma OAI.MatchingFPRAS.Variation.uniform_sum line 73
  10. def OAI.MatchingFPRAS.Variation.imageLaw line 77
  11. lemma OAI.MatchingFPRAS.Variation.imageLaw_nonneg line 80
  12. lemma OAI.MatchingFPRAS.Variation.imageLaw_sum line 82
  13. lemma OAI.MatchingFPRAS.Variation.imageLaw_eq_count line 85
  14. lemma OAI.MatchingFPRAS.Variation.imageLaw_equiv line 93
  15. lemma OAI.MatchingFPRAS.Variation.imageLaw_comp_equiv line 100
  16. lemma OAI.MatchingFPRAS.Variation.push_comp line 107
  17. lemma OAI.MatchingFPRAS.Variation.imageLaw_comp line 125
  18. lemma OAI.MatchingFPRAS.Variation.uniform_prod line 128
  19. lemma OAI.MatchingFPRAS.Variation.imageLaw_pair line 134
  20. lemma OAI.MatchingFPRAS.Variation.bind_push line 145
  21. lemma OAI.MatchingFPRAS.Variation.imageLaw_adaptive_pair line 155
  22. theorem OAI.MatchingFPRAS.Variation.uniform_sigma line 159
  23. lemma OAI.MatchingFPRAS.Variation.imageLaw_ignore line 180
  24. lemma OAI.MatchingFPRAS.Variation.push_sigmaLift line 187
  25. lemma OAI.MatchingFPRAS.Variation.imageLaw_subsingleton line 198
  26. lemma OAI.MatchingFPRAS.Variation.tv_self line 206
  27. lemma OAI.MatchingFPRAS.Variation.imageLaw_fin_skip line 210
  28. def OAI.MatchingFPRAS.WeightedOptions.draw line 233
  29. lemma OAI.MatchingFPRAS.WeightedOptions.chooseBits_imageLaw line 237
  30. lemma OAI.MatchingFPRAS.WeightedOptions.realLaw_push line 249
  31. theorem OAI.MatchingFPRAS.WeightedOptions.draw_tv line 255
  32. def OAI.MatchingFPRAS.WeightedOptions.runDraw line 269
  33. def OAI.MatchingFPRAS.WeightedOptions.exactRun line 274
  34. lemma OAI.MatchingFPRAS.WeightedOptions.exactRun_nonneg line 278
  35. lemma OAI.MatchingFPRAS.WeightedOptions.exactRun_sum line 284
  36. lemma OAI.MatchingFPRAS.WeightedOptions.runDraw_law line 291
  37. theorem OAI.MatchingFPRAS.WeightedOptions.runDraw_tv line 305