OAI/Combinatorics/BalancedRyser/Probability/CoverCountingExposure.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CoverCountingExposure.Marked line 16
  2. theorem OAI.Balanced.CoverCountingExposure.order_sq_le_card_unused line 22
  3. theorem OAI.Balanced.CoverCountingExposure.conditional_mark_le line 35
  4. theorem OAI.Balanced.CoverCountingExposure.past_event_and_mark_le line 59
  5. def OAI.Balanced.CoverCountingExposure.pastUncovered line 84
  6. theorem OAI.Balanced.CoverCountingExposure.pastUncovered_eq_of_history line 88
  7. theorem OAI.Balanced.CoverCountingExposure.pastUncovered_eq_of_larger_history line 93
  8. theorem OAI.Balanced.CoverCountingExposure.earlier_cover_mark_iff line 101
  9. theorem OAI.Balanced.CoverCountingExposure.earlier_deletion_mark_iff line 109
  10. def OAI.Balanced.CoverCountingExposure.priorMixedMarks line 116
  11. theorem OAI.Balanced.CoverCountingExposure.priorMixedMarks_iff_of_history line 124
  12. theorem OAI.Balanced.CoverCountingExposure.past_event_and_actual_mark_le line 150
  13. theorem OAI.Balanced.CoverCountingExposure.prior_mixed_marks_and_actual_mark_le line 163
  14. theorem OAI.Balanced.CoverCountingExposure.measureReal_past_event_and_actual_mark_le line 184
  15. theorem OAI.Balanced.CoverCountingExposure.measure_actual_mark_inter_past_le line 199
  16. theorem OAI.Balanced.CoverCountingExposure.witness_marginal line 220
  17. theorem OAI.Balanced.CoverCountingExposure.witness_and_order_law line 227
  18. theorem OAI.Balanced.CoverCountingExposure.independent_outer_past_event_and_actual_mark_le line 240