OAI/Combinatorics/BalancedRyser/Probability/UnusedOffsetAveraging.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.UnusedOffsetIncidence.pmf_sum_real line 11
2. theorem OAI.Balanced.UnusedOffsetIncidence.pmf_outer_ne_top line 18
3. theorem OAI.Balanced.UnusedOffsetIncidence.bind_probability_le line 23
4. theorem OAI.Balanced.UnusedOffsetIncidence.uniform_product_probability_le line 37
5. def OAI.Balanced.UnusedOffsetIncidence.mixedUnusedLaw line 49
6. theorem OAI.Balanced.UnusedOffsetIncidence.mixed_precoverage_probability_le line 53
7. theorem OAI.Balanced.UnusedOffsetIncidence.mixed_noncollinearTriple_probability_le line 69
8. theorem OAI.Balanced.UnusedOffsetIncidence.uniform_product_noncollinearTriple_probability_le line 85