OAI/Combinatorics/BalancedRyser/Probability/ThinningTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.BernoulliTail.tendsto_polynomial_mul_ratio_tail line 10
2. def OAI.Balanced.BernoulliTail.thinningCutoff line 26
3. lemma OAI.Balanced.BernoulliTail.rpow_lt_thinningCutoff line 29
4. lemma OAI.Balanced.BernoulliTail.tendsto_thinningCutoff_atTop line 33
5. lemma OAI.Balanced.BernoulliTail.eventually_log_le_thinningCutoff line 38
6. lemma OAI.Balanced.BernoulliTail.tendsto_polynomial_mul_thinning_tail line 47
7. lemma OAI.Balanced.BernoulliTail.tendsto_post_step_abort_bound line 54
8. lemma OAI.Balanced.BernoulliTail.tendsto_polynomial_mul_factorial_thinning_tail line 61
9. lemma OAI.Balanced.BernoulliTail.tendsto_thinning_test_union line 74