OAI/Combinatorics/BalancedRyser/Deletion/SelectedDeletionEventsLemmas.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.SelectedDeletion.sum_deletionEventIndicator line 15
  2. theorem OAI.Balanced.SelectedDeletion.sum_event_deletionJointMass line 38
  3. theorem OAI.Balanced.SelectedDeletion.realizingLaw_eventProbability line 70
  4. theorem OAI.Balanced.SelectedDeletion.jointMass_eq_success_mul_eventProbability line 87
  5. theorem OAI.Balanced.SelectedDeletion.realizingLaw_unique line 109
  6. theorem OAI.Balanced.SelectedDeletion.realizingLaw_successMass_ne_zero line 116
  7. theorem OAI.Balanced.SelectedDeletion.realizingLaw_successMass_pos line 127
  8. theorem OAI.Balanced.SelectedDeletion.realizingLaw_eq_conditionalDeletionLaw line 133
  9. theorem OAI.Balanced.SelectedDeletion.existsUnique_realizingLaw_iff line 139
  10. theorem OAI.Balanced.SelectedDeletion.not_realizingLaw_of_successMass_zero line 150
  11. theorem OAI.Balanced.SelectedDeletion.uniformDeletionMass_three_pos line 165
  12. theorem OAI.Balanced.SelectedDeletion.realizesConditionalLaw_ratio_le line 172
  13. theorem OAI.Balanced.SelectedDeletion.conditionalDeletionLaw_ratio_le line 209