OAI/Probability/Ballisticity/Estimates/CommonOffset.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.sharedNoDropMass_positive line 159
2. lemma OAI.DirectionalTransience.commonOffset_exists line 166
3. def OAI.DirectionalTransience.commonOffset line 174
4. lemma OAI.DirectionalTransience.measurable_commonOffset line 177
5. lemma OAI.DirectionalTransience.commonOffset_spec line 186
6. lemma OAI.DirectionalTransience.commonOffset_min line 191
7. lemma OAI.DirectionalTransience.commonOffset_gt_subset line 195
8. lemma OAI.DirectionalTransience.shared_common_boundary_exists line 205
9. theorem OAI.DirectionalTransience.shared_common_displacement_small line 235
10. lemma OAI.DirectionalTransience.symmetric_summand_tail line 290
11. theorem OAI.DirectionalTransience.iid_symmetric_sum_spread line 323