OAI/Probability/SpanningForest/SchauderTail.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem336.SchauderTail.measure_abs_gt_le_fourth_moment line 14
2. lemma OAI.Problem336.SchauderTail.fourth_threshold_identity line 32
3. lemma OAI.Problem336.SchauderTail.measure_bad_block_le line 43
4. theorem OAI.Problem336.SchauderTail.ae_eventually_dyadic_bound line 74
5. theorem OAI.Problem336.SchauderTail.ae_eventually_gaussian_dyadic_bound line 88
6. def OAI.Problem336.SchauderTail.incrementRatio line 102
7. lemma OAI.Problem336.SchauderTail.incrementRatio_nonneg line 104
8. lemma OAI.Problem336.SchauderTail.incrementRatio_lt_one line 108
9. lemma OAI.Problem336.SchauderTail.summable_incrementRatio line 114
10. theorem OAI.Problem336.SchauderTail.ae_eventually_gaussian_increment_bound line 117
11. theorem OAI.Problem336.SchauderTail.ae_all_eventually_gaussian_increment_bound line 143