OAI/Combinatorics/Ryser/Selection/Estimates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Selection.sum_le_card_mul_add_bad_card_mul line 14
  2. theorem OAI.RyserCoveringCounterexample.Selection.mass_after_chunk_ge line 32
  3. theorem OAI.RyserCoveringCounterexample.Selection.mass_ge_geometric_sub_error line 61
  4. theorem OAI.RyserCoveringCounterexample.Selection.mass_after_chunks_ge_density line 80
  5. theorem OAI.RyserCoveringCounterexample.Selection.unused_weight_ge line 100
  6. theorem OAI.RyserCoveringCounterexample.Selection.prod_one_sub_pow_le_exp_neg_sum line 122
  7. theorem OAI.RyserCoveringCounterexample.Selection.unused_failure_product_le line 139