OAI/Probability/Ballisticity/Estimates/FluctuationScaleUpperMultiple.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.fluctuationScale_upper_multiple line 262
2. theorem OAI.DirectionalTransience.gaussian_sequence_uniform_good line 278
3. theorem OAI.DirectionalTransience.gaussian_bad_radii_sublinear line 299
4. lemma OAI.DirectionalTransience.sqrt_quadratic_minorant line 322
5. lemma OAI.DirectionalTransience.clipped_three_halves_minorant line 334
6. lemma OAI.DirectionalTransience.gaussian_fourth_moment line 373
7. lemma OAI.DirectionalTransience.gaussian_second_moment line 412
8. lemma OAI.DirectionalTransience.clipped_three_halves_continuous line 417
9. lemma OAI.DirectionalTransience.clipped_three_halves_integrable line 422
10. theorem OAI.DirectionalTransience.gaussian_clipped_drift line 431