OAI/Combinatorics/BalancedRyser/Probability/BernoulliTail.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.esymm_cons_succ line 13
2. lemma OAI.Balanced.factorial_mul_esymm_le_sum_pow line 18
3. lemma OAI.Balanced.sum_prod_powersetCard_le line 41
4. lemma OAI.Balanced.pow_div_factorial_le_exp_ratio line 53
5. def OAI.Balanced.BernoulliTail.countEvents line 73
6. lemma OAI.Balanced.BernoulliTail.countEvents_ge_iff line 77
7. lemma OAI.Balanced.BernoulliTail.choose_countEvents_eq_sum line 94
8. lemma OAI.Balanced.BernoulliTail.integral_choose_countEvents line 107
9. lemma OAI.Balanced.BernoulliTail.count_tail_le_moment line 122
10. lemma OAI.Balanced.BernoulliTail.independent_count_tail_le line 142
11. lemma OAI.Balanced.BernoulliTail.independent_count_tail_chain line 166
12. lemma OAI.Balanced.BernoulliTail.independent_count_tail_exp_bound line 184