OAI/Combinatorics/Ryser/Selection/ChunkTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Selection.equationBound line 18
  2. def OAI.RyserCoveringCounterexample.Selection.regularTailConstant line 20
  3. def OAI.RyserCoveringCounterexample.Selection.RegularEntry line 23
  4. def OAI.RyserCoveringCounterexample.Selection.regularEntries line 28
  5. theorem OAI.RyserCoveringCounterexample.Selection.regularTailConstant_nonneg line 34
  6. theorem OAI.RyserCoveringCounterexample.Selection.prob_regular_entry_gt_le line 39
  7. theorem OAI.RyserCoveringCounterexample.Selection.card_irregularEntries_le line 74
  8. theorem OAI.RyserCoveringCounterexample.Selection.prob_many_regular_exceedances_le line 86
  9. theorem OAI.RyserCoveringCounterexample.Selection.chunk_recurrence_of_few_regular_exceedances line 115
  10. theorem OAI.RyserCoveringCounterexample.Selection.prob_chunk_recurrence_failure_le line 171