OAI/Combinatorics/BalancedRyser/Local/LocalPatternEvents.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.LargePencilEvent line 11
  2. def OAI.Balanced.Local.HighReuseEvent line 14
  3. def OAI.Balanced.Local.SmallBadPatternEvent line 17
  4. theorem OAI.Balanced.Local.positive_kernel_local_failure_cases line 29
  5. theorem OAI.Balanced.Local.selectedProbability_le_three_of_positive_imp line 57
  6. theorem OAI.Balanced.Local.local_failure_probability_le line 88