OAI/Combinatorics/Ryser/LineCover/TupleConcentration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RyserCoveringCounterexample.LineCover.countTailConstant line 13
2. def OAI.RyserCoveringCounterexample.LineCover.tupleTailConstant line 17
3. theorem OAI.RyserCoveringCounterexample.LineCover.countTailConstant_pos line 20
4. theorem OAI.RyserCoveringCounterexample.LineCover.tupleTailConstant_pos line 28
5. theorem OAI.RyserCoveringCounterexample.LineCover.variance_budget_real line 34
6. theorem OAI.RyserCoveringCounterexample.LineCover.tail_exponent_identity line 49
7. theorem OAI.RyserCoveringCounterexample.LineCover.retainedCount_square_lower_tail line 87
8. theorem OAI.RyserCoveringCounterexample.LineCover.admissibleTuple_lower_tail line 147
9. theorem OAI.RyserCoveringCounterexample.LineCover.prob_exists_admissibleTuple_bad_le line 166
10. theorem OAI.RyserCoveringCounterexample.LineCover.card_lineTuple_le line 202
11. theorem OAI.RyserCoveringCounterexample.LineCover.prob_exists_admissibleTuple_bad_le_card_bound line 218