OAI/Combinatorics/BalancedRyser/Deletion/DeletionCountingExposure.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.DeletionCountingExposure.observation line 17
  2. theorem OAI.Balanced.DeletionCountingExposure.mem_countingHistory_iff_observation_eq line 21
  3. theorem OAI.Balanced.DeletionCountingExposure.fiberMean_eq_history line 55
  4. theorem OAI.Balanced.DeletionCountingExposure.expect_history_tower line 72
  5. theorem OAI.Balanced.DeletionCountingExposure.nextLine_eq_of_history line 81
  6. def OAI.Balanced.DeletionCountingExposure.exposedLines line 88
  7. theorem OAI.Balanced.DeletionCountingExposure.exposedLines_eq_of_history line 92
  8. def OAI.Balanced.DeletionCountingExposure.pastUncovered line 102
  9. theorem OAI.Balanced.DeletionCountingExposure.pastUncovered_eq_of_history line 106
  10. theorem OAI.Balanced.DeletionCountingExposure.earlier_deletion_mark_iff line 113
  11. theorem OAI.Balanced.DeletionCountingExposure.earlier_cover_mark_iff line 123
  12. def OAI.Balanced.DeletionCountingExposure.priorMixedMarks line 131
  13. theorem OAI.Balanced.DeletionCountingExposure.priorMixedMarks_iff_of_history line 142
  14. theorem OAI.Balanced.DeletionCountingExposure.sum_remainingTokens_eq line 173
  15. theorem OAI.Balanced.DeletionCountingExposure.marked_iff line 181
  16. theorem OAI.Balanced.DeletionCountingExposure.conditional_event_and_mark_le line 185
  17. theorem OAI.Balanced.DeletionCountingExposure.past_event_and_mark_le line 218
  18. theorem OAI.Balanced.DeletionCountingExposure.past_event_and_actual_mark_le line 240
  19. theorem OAI.Balanced.DeletionCountingExposure.prior_mixed_marks_and_actual_mark_le line 259
  20. theorem OAI.Balanced.DeletionCountingExposure.independent_outer_past_event_and_actual_mark_le line 284