OAI/Combinatorics/BalancedRyser/Probability/SelectedExperimentLaw.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.SelectedDeletion.ExperimentAudit.outcomeWeight line 13
  2. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.outcomeWeight_nonneg line 17
  3. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.sum_outcomeWeight line 24
  4. def OAI.Balanced.SelectedDeletion.ExperimentAudit.fixedOutcomeLaw line 30
  5. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.fixedOutcomeLaw_real line 37
  6. def OAI.Balanced.SelectedDeletion.ExperimentAudit.experimentLaw line 42
  7. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.offset_marginal line 46
  8. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.experimentLaw_apply line 54
  9. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.experimentLaw_real line 61
  10. def OAI.Balanced.SelectedDeletion.ExperimentAudit.returnedEvent line 67
  11. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.returnedEvent_probability line 71
  12. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.success_probability line 85
  13. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.fixedOutcomeLaw_of_bad_initial line 89
  14. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.offset_event_probability line 98
  15. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.successful_atom_supported line 105
  16. theorem OAI.Balanced.SelectedDeletion.ExperimentAudit.deletion_atom_probability line 117