OAI/Combinatorics/MatchingCount/Probability/AdaptiveLaw.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingFPRAS.Counting.trial_output_error line 8
  2. lemma OAI.MatchingFPRAS.UnitRefresh.pairingCount_le_half_power line 30
  3. lemma OAI.MatchingFPRAS.Trial.initial_raw_partition line 47
  4. theorem OAI.MatchingFPRAS.Trial.final_padding line 51
  5. theorem OAI.MatchingFPRAS.Trial.final_trial_interval line 86
  6. structure OAI.MatchingFPRAS.Adaptive.Law line 116
  7. instance OAI.MatchingFPRAS.Adaptive.(instance at line 121) line 121
  8. def OAI.MatchingFPRAS.Adaptive.Law.event line 123
  9. lemma OAI.MatchingFPRAS.Adaptive.Law.event_nonneg line 127
  10. lemma OAI.MatchingFPRAS.Adaptive.Law.event_le_one line 135
  11. def OAI.MatchingFPRAS.Adaptive.Law.step line 144
  12. lemma OAI.MatchingFPRAS.Adaptive.Law.step_event line 151
  13. theorem OAI.MatchingFPRAS.Adaptive.first_failure_step line 162
  14. def OAI.MatchingFPRAS.Adaptive.Law.evolve line 181
  15. theorem OAI.MatchingFPRAS.Adaptive.first_failure_bound line 185
  16. theorem OAI.MatchingFPRAS.Adaptive.source_trial_failure line 197
  17. def OAI.MatchingFPRAS.Adaptive.Law.sigma line 213
  18. lemma OAI.MatchingFPRAS.Adaptive.Law.sigma_event line 222
  19. lemma OAI.MatchingFPRAS.Adaptive.Law.event_mono line 233
  20. lemma OAI.MatchingFPRAS.Adaptive.first_failure_sigma line 244
  21. def OAI.MatchingFPRAS.Adaptive.Law.changeFintype line 271
  22. theorem OAI.MatchingFPRAS.Adaptive.Law.changeFintype_mass line 276
  23. def OAI.MatchingFPRAS.Adaptive.Law.iid line 282
  24. def OAI.MatchingFPRAS.Enlargement.sourceRunLawBase line 302
  25. def OAI.MatchingFPRAS.Enlargement.sourceRunLaw line 309
  26. lemma OAI.MatchingFPRAS.Enlargement.sourceRunLaw_mass line 315
  27. def OAI.MatchingFPRAS.Enlargement.sourceMarkedFintype line 324
  28. theorem OAI.MatchingFPRAS.Enlargement.sourceRunLaw_budget line 326
  29. structure OAI.MatchingFPRAS.Trial.Parameters line 354
  30. lemma OAI.MatchingFPRAS.Trial.Parameters.K_pos line 372
  31. lemma OAI.MatchingFPRAS.Trial.Parameters.epsilon_real_pos line 375
  32. lemma OAI.MatchingFPRAS.Trial.Parameters.epsilon_real_lt_one line 378
  33. def OAI.MatchingFPRAS.Trial.Parameters.D line 380
  34. def OAI.MatchingFPRAS.Trial.Parameters.N line 382
  35. lemma OAI.MatchingFPRAS.Trial.Parameters.N_pos line 385
  36. lemma OAI.MatchingFPRAS.Trial.Parameters.D_pos line 390
  37. def OAI.MatchingFPRAS.Trial.Parameters.T line 392
  38. def OAI.MatchingFPRAS.Trial.Parameters.q line 394
  39. lemma OAI.MatchingFPRAS.Trial.Parameters.q_pos line 396
  40. def OAI.MatchingFPRAS.Trial.Parameters.sigma line 402
  41. def OAI.MatchingFPRAS.Trial.Parameters.S line 404
  42. def OAI.MatchingFPRAS.Trial.Parameters.initialData line 406
  43. lemma OAI.MatchingFPRAS.Trial.Parameters.sigma_pos line 410
  44. lemma OAI.MatchingFPRAS.Trial.Parameters.S_pos line 412
  45. lemma OAI.MatchingFPRAS.Trial.Parameters.S_bound line 414
  46. lemma OAI.MatchingFPRAS.Trial.sourcePM_nonempty line 417
  47. def OAI.MatchingFPRAS.Trial.ScaleState.start line 425
  48. def OAI.MatchingFPRAS.Trial.ScaleState.runLaw line 428
  49. def OAI.MatchingFPRAS.Trial.ScaleState.sampleLaw line 433
  50. theorem OAI.MatchingFPRAS.Trial.ScaleState.sampleLaw_budget line 436
  51. structure OAI.MatchingFPRAS.Trial.Layer line 444
  52. def OAI.MatchingFPRAS.Trial.Layer.good line 454
  53. def OAI.MatchingFPRAS.Trial.firstLayer line 458
  54. def OAI.MatchingFPRAS.Trial.Layer.append line 466
  55. theorem OAI.MatchingFPRAS.Trial.Layer.append_good line 477
  56. theorem OAI.MatchingFPRAS.Trial.Layer.append_failure line 489
  57. def OAI.MatchingFPRAS.Trial.layers line 500
  58. theorem OAI.MatchingFPRAS.Trial.layers_failure line 504
  59. def OAI.MatchingFPRAS.Trial.output line 520
  60. lemma OAI.MatchingFPRAS.Trial.output_nonneg line 523
  61. def OAI.MatchingFPRAS.Trial.Accurate line 527
  62. theorem OAI.MatchingFPRAS.Trial.good_output line 530
  63. theorem OAI.MatchingFPRAS.Trial.actual_ideal_trial_failure line 535