OAI/Probability/Ballisticity/Walk/WienerPathMaximal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.gaussian_independent_sum_range_law line 16
2. lemma OAI.DirectionalTransience.gaussian_martingale_maximal_le line 40
3. lemma OAI.DirectionalTransience.gaussian_martingale_abs_maximal_le line 68
4. lemma OAI.DirectionalTransience.fin_sum_Iic_eq_range line 89
5. lemma OAI.DirectionalTransience.gaussian_pi_prefix_maximal line 103
6. lemma OAI.DirectionalTransience.gaussianPathFiniteLaw_abs_maximal line 147
7. lemma OAI.DirectionalTransience.wiener_path_finite_abs_maximal line 187
8. lemma OAI.DirectionalTransience.wiener_path_countable_abs_maximal line 211
9. lemma OAI.DirectionalTransience.wiener_path_abs_gt_maximal line 248
10. lemma OAI.DirectionalTransience.wiener_path_abs_maximal line 265
11. lemma OAI.DirectionalTransience.wiener_path_norm_maximal line 292
12. lemma OAI.DirectionalTransience.distribution_path_norm_limsup line 306