OAI/Combinatorics/MatchingCount/Sampling/Certify.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Counting.sigma_nonneg line 9
  2. lemma OAI.MatchingFPRAS.Counting.sigma_small line 12
  3. lemma OAI.MatchingFPRAS.Counting.sigma_times_D line 19
  4. lemma OAI.MatchingFPRAS.Counting.sigma_relative line 26
  5. lemma OAI.MatchingFPRAS.Counting.ratio_error line 32
  6. lemma OAI.MatchingFPRAS.Counting.upper_error line 65
  7. theorem OAI.MatchingFPRAS.Counting.successful_stage_estimates line 118
  8. instance OAI.MatchingFPRAS.Transport.Sparse.decideMatching line 151
  9. def OAI.MatchingFPRAS.Transport.Sparse.certify line 156
  10. lemma OAI.MatchingFPRAS.Transport.Sparse.mem_certify line 159
  11. lemma OAI.MatchingFPRAS.Transport.Sparse.card_certify line 162
  12. def OAI.MatchingFPRAS.Transport.Sparse.colorRaw line 166
  13. def OAI.MatchingFPRAS.Transport.Sparse.colors line 170
  14. lemma OAI.MatchingFPRAS.Transport.Sparse.mem_colorRaw line 174
  15. lemma OAI.MatchingFPRAS.Transport.Sparse.mem_colors line 183
  16. lemma OAI.MatchingFPRAS.Transport.Sparse.colors_eq line 193
  17. lemma OAI.MatchingFPRAS.Transport.Sparse.colorRaw_card line 199
  18. def OAI.MatchingFPRAS.Transport.Sparse.switchPatterns line 208
  19. def OAI.MatchingFPRAS.Transport.Sparse.switchRaw line 213
  20. def OAI.MatchingFPRAS.Transport.Sparse.switches line 216
  21. lemma OAI.MatchingFPRAS.Transport.Sparse.mem_switches line 219
  22. lemma OAI.MatchingFPRAS.Transport.Sparse.switches_eq line 232
  23. lemma OAI.MatchingFPRAS.Transport.Sparse.switchRaw_card line 237
  24. theorem OAI.MatchingFPRAS.Transport.Sparse.colors_card line 244
  25. theorem OAI.MatchingFPRAS.Transport.Sparse.switches_card line 249
  26. def OAI.MatchingFPRAS.ComputableReach.grow line 264
  27. def OAI.MatchingFPRAS.ComputableReach.reached line 266
  28. def OAI.MatchingFPRAS.ComputableReach.closure line 268
  29. lemma OAI.MatchingFPRAS.ComputableReach.mem_grow line 270
  30. lemma OAI.MatchingFPRAS.ComputableReach.subset_grow line 273
  31. lemma OAI.MatchingFPRAS.ComputableReach.grow_mono line 275
  32. lemma OAI.MatchingFPRAS.ComputableReach.reached_step line 281
  33. lemma OAI.MatchingFPRAS.ComputableReach.reached_step' line 284
  34. lemma OAI.MatchingFPRAS.ComputableReach.reached_succ line 287
  35. lemma OAI.MatchingFPRAS.ComputableReach.reached_mono_time line 291
  36. lemma OAI.MatchingFPRAS.ComputableReach.reached_reachable line 294
  37. lemma OAI.MatchingFPRAS.ComputableReach.walk_reached line 306
  38. theorem OAI.MatchingFPRAS.ComputableReach.mem_closure line 314
  39. def OAI.MatchingFPRAS.ComputableReach.cellsWritten line 321
  40. lemma OAI.MatchingFPRAS.ComputableReach.cellsWritten_bound line 324