OAI/Combinatorics/BalancedRyser/Selection/SelectionFirstAbort.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Selection.Process.FirstAbort.StateConcentration line 17
  2. def OAI.Balanced.Selection.Process.FirstAbort.ConcentratedPath line 26
  3. def OAI.Balanced.Selection.Process.FirstAbort.NoPostAbort line 30
  4. def OAI.Balanced.Selection.Process.FirstAbort.SupportedPath line 35
  5. theorem OAI.Balanced.Selection.Process.FirstAbort.ae_supportedPath line 40
  6. theorem OAI.Balanced.Selection.Process.FirstAbort.next_state_of_checks line 57
  7. theorem OAI.Balanced.Selection.Process.FirstAbort.survives_of_checks line 75
  8. theorem OAI.Balanced.Selection.Process.FirstAbort.precheck_of_stateConcentration line 89
  9. theorem OAI.Balanced.Selection.Process.FirstAbort.survives_of_concentration line 106
  10. theorem OAI.Balanced.Selection.Process.FirstAbort.ae_survives_of_concentration line 123
  11. theorem OAI.Balanced.Selection.Process.FirstAbort.main_failure_probability_le line 136
  12. theorem OAI.Balanced.Selection.Process.FirstAbort.exists_firstAbort_threshold line 167