OAI/Probability/Ballisticity/Walk/GaussianPathFiniteLawSmul.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.gaussianPathFiniteLaw_smul line 46
2. lemma OAI.DirectionalTransience.median_div line 79
3. def OAI.DirectionalTransience.heightPathLaw line 92
4. lemma OAI.DirectionalTransience.heightPathLaw_iid_difference line 98
5. lemma OAI.DirectionalTransience.heightPathLaw_restrict line 110
6. theorem OAI.DirectionalTransience.height_median_path_limit line 122