OAI/Combinatorics/BalancedRyser/Selection/SelectionSuccessBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Selection.Process.not_noPostAbort_eq_union line 18
  2. theorem OAI.Balanced.Selection.Process.successMass_finalLaw_ge_good_events line 45
  3. theorem OAI.Balanced.Selection.Process.successMass_finalLaw_ge_concentration_sub_postcheck line 79
  4. theorem OAI.Balanced.Selection.Process.successMass_outputLaw_ge_concentration_sub_postcheck line 97
  5. theorem OAI.Balanced.Selection.Process.exists_uniform_success_threshold line 115