OAI/Combinatorics/BalancedRyser/Selection/SelectionLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Selection.successMass_nonnegative line 18
  2. theorem OAI.Balanced.Selection.successMass_le_one line 21
  3. theorem OAI.Balanced.Selection.outcomeWeight_nonnegative line 23
  4. theorem OAI.Balanced.Selection.sum_outcomeWeight line 28
  5. def OAI.Balanced.Selection.OutputLaw.toPMF line 33
  6. theorem OAI.Balanced.Selection.toPMF_none line 39
  7. theorem OAI.Balanced.Selection.toPMF_some line 41
  8. theorem OAI.Balanced.Selection.toPMF_some_real line 43
  9. theorem OAI.Balanced.Selection.weight_eq_zero_of_not_transversal line 46
  10. theorem OAI.Balanced.Selection.positive_output_is_transversal line 52
  11. theorem OAI.Balanced.Selection.returned_finset_probability line 57
  12. theorem OAI.Balanced.Selection.success_probability line 69
  13. theorem OAI.Balanced.Selection.cylinder_probability line 75
  14. theorem OAI.Balanced.Selection.impossible_cylinder_zero line 82
  15. theorem OAI.Balanced.Selection.occupancy_failure_probability line 90