OAI/Probability/Ballisticity/Estimates/NonCollapsedSums.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.iid_fluctuation_not_collapse line 13
2. lemma OAI.DirectionalTransience.double_floor_ratio line 56
3. lemma OAI.DirectionalTransience.inMeasure_sub_zero line 70
4. def OAI.DirectionalTransience.dyadicCut line 99
5. lemma OAI.DirectionalTransience.dyadicCut_pos line 100
6. lemma OAI.DirectionalTransience.dyadicCut_le_one line 101
7. lemma OAI.DirectionalTransience.dyadicCut_antitone line 102
8. lemma OAI.DirectionalTransience.dyadicCut_tendsto line 105
9. lemma OAI.DirectionalTransience.variance_ratio_unit line 108
10. lemma OAI.DirectionalTransience.exists_dyadic_variance_profile line 119