OAI/Combinatorics/BalancedRyser/Probability/ScheduledCountingExposure.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ScheduledCountingExposure.DExperiment line 23
  2. abbrev OAI.Balanced.ScheduledCountingExposure.Sample line 26
  3. abbrev OAI.Balanced.ScheduledCountingExposure.Steps line 29
  4. def OAI.Balanced.ScheduledCountingExposure.pastD line 32
  5. def OAI.Balanced.ScheduledCountingExposure.pastC line 35
  6. def OAI.Balanced.ScheduledCountingExposure.uncovered line 38
  7. def OAI.Balanced.ScheduledCountingExposure.target line 43
  8. def OAI.Balanced.ScheduledCountingExposure.Mark line 47
  9. def OAI.Balanced.ScheduledCountingExposure.markCount line 51
  10. def OAI.Balanced.ScheduledCountingExposure.arrayUncovered line 54
  11. def OAI.Balanced.ScheduledCountingExposure.arrayMark line 58
  12. def OAI.Balanced.ScheduledCountingExposure.arrayMarkCount line 63
  13. theorem OAI.Balanced.ScheduledCountingExposure.mark_eq_arrayMark line 67
  14. theorem OAI.Balanced.ScheduledCountingExposure.markCount_eq_arrayMarkCount line 77
  15. theorem OAI.Balanced.ScheduledCountingExposure.pastD_mono line 84
  16. theorem OAI.Balanced.ScheduledCountingExposure.pastC_mono line 92
  17. theorem OAI.Balanced.ScheduledCountingExposure.deletion_position_mem line 100
  18. theorem OAI.Balanced.ScheduledCountingExposure.cover_position_mem line 106
  19. theorem OAI.Balanced.ScheduledCountingExposure.deletion_position_not_mem line 111
  20. theorem OAI.Balanced.ScheduledCountingExposure.cover_position_not_mem line 116
  21. theorem OAI.Balanced.ScheduledCountingExposure.uncovered_eq_D line 121
  22. theorem OAI.Balanced.ScheduledCountingExposure.uncovered_eq_C line 126
  23. theorem OAI.Balanced.ScheduledCountingExposure.mark_iff_D_history line 131
  24. theorem OAI.Balanced.ScheduledCountingExposure.mark_iff_C_history line 148
  25. def OAI.Balanced.ScheduledCountingExposure.Cylinder line 165
  26. theorem OAI.Balanced.ScheduledCountingExposure.cylinder_iff_D_history line 169
  27. theorem OAI.Balanced.ScheduledCountingExposure.cylinder_iff_C_history line 180
  28. theorem OAI.Balanced.ScheduledCountingExposure.activeD_remaining line 193
  29. theorem OAI.Balanced.ScheduledCountingExposure.pastC_card_le line 212
  30. theorem OAI.Balanced.ScheduledCountingExposure.expect_sample line 218
  31. theorem OAI.Balanced.ScheduledCountingExposure.expect_sample_swap line 224
  32. theorem OAI.Balanced.ScheduledCountingExposure.step_expect_le line 229
  33. theorem OAI.Balanced.ScheduledCountingExposure.sampleNonempty line 280
  34. theorem OAI.Balanced.ScheduledCountingExposure.step_measure_le line 287
  35. theorem OAI.Balanced.ScheduledCountingExposure.markCount_tail_measure_le line 311
  36. theorem OAI.Balanced.ScheduledCountingExposure.markCount_tail_expect_le line 331
  37. theorem OAI.Balanced.ScheduledCountingExposure.rare_mark_expect_le line 347
  38. theorem OAI.Balanced.ScheduledCountingExposure.markCount_eq_zero_of_one_le_cutoff line 368
  39. theorem OAI.Balanced.ScheduledCountingExposure.rare_mark_expect_le_all_cutoffs line 376
  40. theorem OAI.Balanced.ScheduledCountingExposure.uniform_rare_mark_bound line 394