OAI/Probability/Ballisticity/Estimates/BoundaryDecorrelation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.pairSide line 14
2. lemma OAI.DirectionalTransience.measurable_pairSide line 16
3. lemma OAI.DirectionalTransience.measurable_pairSide_recenter line 20
4. lemma OAI.DirectionalTransience.shared_boundary_test_decorrelation line 25
5. lemma OAI.DirectionalTransience.uniform_eventually_of_all_sequences line 86
6. lemma OAI.DirectionalTransience.integral_bounded_test_tendsto line 96
7. theorem OAI.DirectionalTransience.shared_path_marginal_tests_uniform line 106