OAI/Probability/Ballisticity/Walk/SharedPairPathLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.probability_law_tendsto line 16
2. theorem OAI.DirectionalTransience.shared_pair_path_limit line 31
3. lemma OAI.DirectionalTransience.medianFirstHitPath_sub_linear line 107
4. lemma OAI.DirectionalTransience.linear_add_median_error line 115
5. lemma OAI.DirectionalTransience.median_center_error_tendsto line 124
6. theorem OAI.DirectionalTransience.shared_median_pair_path_limit line 143