OAI/Combinatorics/BalancedRyser/Deletion/SelectedDeletionPMF.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.SelectedDeletion.jointMass_nonneg line 14
  2. theorem OAI.Balanced.SelectedDeletion.successMass_nonneg line 26
  3. theorem OAI.Balanced.SelectedDeletion.deletionJointMass_nonneg line 29
  4. theorem OAI.Balanced.SelectedDeletion.sum_deletionIndicator line 33
  5. theorem OAI.Balanced.SelectedDeletion.sum_deletionJointMass line 57
  6. theorem OAI.Balanced.SelectedDeletion.sum_normalizedDeletionJointMass line 73
  7. def OAI.Balanced.SelectedDeletion.conditionalDeletionLaw line 79
  8. theorem OAI.Balanced.SelectedDeletion.conditionalDeletionLaw_apply_toReal line 87
  9. theorem OAI.Balanced.SelectedDeletion.conditionalDeletionLaw_realizes line 94
  10. theorem OAI.Balanced.SelectedDeletion.exists_realizing_dominated_law line 99