OAI/Probability/Ballisticity/Estimates/GridLinear.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.GridLinear line 42
2. lemma OAI.DirectionalTransience.isClosed_gridLinear line 47
3. def OAI.DirectionalTransience.pathRestrictScale line 67
4. lemma OAI.DirectionalTransience.pathRestrictScale_apply line 70
5. lemma OAI.DirectionalTransience.gridLinear_uniform_on_shorter line 73
6. lemma OAI.DirectionalTransience.weak_sub_const_tendsto line 153
7. lemma OAI.DirectionalTransience.weak_sequence_tight line 175
8. lemma OAI.DirectionalTransience.GridLinear.sub line 187
9. theorem OAI.DirectionalTransience.path_grid_median_limit_from_iid_difference line 193