OAI/Combinatorics/MatchingCount/Graphs/Cumulative.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.FiniteChoice.cumulative line 26
  2. lemma OAI.MatchingFPRAS.FiniteChoice.cumulative_zero line 28
  3. lemma OAI.MatchingFPRAS.FiniteChoice.cumulative_total line 30
  4. lemma OAI.MatchingFPRAS.FiniteChoice.options_pos line 33
  5. lemma OAI.MatchingFPRAS.FiniteChoice.cumulative_mono line 39
  6. def OAI.MatchingFPRAS.FiniteChoice.candidates line 48
  7. lemma OAI.MatchingFPRAS.FiniteChoice.candidates_nonempty line 51
  8. def OAI.MatchingFPRAS.FiniteChoice.choose line 61
  9. def OAI.MatchingFPRAS.FiniteChoice.outputLaw line 64
  10. def OAI.MatchingFPRAS.FiniteChoice.gridInterval line 70
  11. lemma OAI.MatchingFPRAS.FiniteChoice.gridInterval_eq line 73
  12. lemma OAI.MatchingFPRAS.FiniteChoice.gridInterval_card line 92
  13. lemma OAI.MatchingFPRAS.FiniteChoice.gridInterval_error line 97
  14. lemma OAI.MatchingFPRAS.FiniteChoice.cumulative_nonneg line 117
  15. lemma OAI.MatchingFPRAS.FiniteChoice.cumulative_le_one line 121
  16. lemma OAI.MatchingFPRAS.FiniteChoice.cumulative_step line 125
  17. lemma OAI.MatchingFPRAS.FiniteChoice.choose_upper line 140
  18. lemma OAI.MatchingFPRAS.FiniteChoice.choose_le line 146
  19. lemma OAI.MatchingFPRAS.FiniteChoice.choose_lower line 151
  20. lemma OAI.MatchingFPRAS.FiniteChoice.choose_eq_iff line 168
  21. lemma OAI.MatchingFPRAS.FiniteChoice.outputLaw_grid line 188
  22. lemma OAI.MatchingFPRAS.FiniteChoice.outputLaw_error line 205
  23. theorem OAI.MatchingFPRAS.FiniteChoice.fixed_bit_choice line 215
  24. lemma OAI.MatchingFPRAS.FiniteChoice.outputLaw_nonneg line 234
  25. lemma OAI.MatchingFPRAS.FiniteChoice.outputLaw_sum line 237
  26. lemma OAI.MatchingFPRAS.FiniteChoice.fixed_bit_l1 line 249
  27. def OAI.MatchingFPRAS.BoundedSimulation.categoricalStep line 266
  28. def OAI.MatchingFPRAS.BoundedSimulation.idealRun line 270
  29. def OAI.MatchingFPRAS.BoundedSimulation.bitRun line 275
  30. lemma OAI.MatchingFPRAS.BoundedSimulation.row_nonneg line 285
  31. lemma OAI.MatchingFPRAS.BoundedSimulation.row_sum line 289
  32. lemma OAI.MatchingFPRAS.BoundedSimulation.step_nonneg line 293
  33. lemma OAI.MatchingFPRAS.BoundedSimulation.step_sum line 298
  34. lemma OAI.MatchingFPRAS.BoundedSimulation.row_l1 line 306
  35. lemma OAI.MatchingFPRAS.BoundedSimulation.step_l1 line 317
  36. lemma OAI.MatchingFPRAS.BoundedSimulation.idealRun_prob line 342
  37. lemma OAI.MatchingFPRAS.BoundedSimulation.bitRun_step_l1 line 353
  38. theorem OAI.MatchingFPRAS.BoundedSimulation.finite_bit_simulation line 369
  39. def OAI.MatchingFPRAS.FiniteChoice.tapeIndex line 395
  40. def OAI.MatchingFPRAS.FiniteChoice.chooseBits line 398
  41. def OAI.MatchingFPRAS.FiniteChoice.tapeLaw line 402