OAI/Probability/Ballisticity/Walk/WeakPathEvalTendsto.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.weak_path_eval_tendsto line 34
2. lemma OAI.DirectionalTransience.gaussian_median_nonstrict line 55
3. lemma OAI.DirectionalTransience.continuous_gaussian_path_mean line 62
4. lemma OAI.DirectionalTransience.weak_path_grid_medians_uniform line 80