OAI/Probability/Ballisticity/Crossings/CommonCutObserver.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.pairOrigin line 15
2. lemma OAI.DirectionalTransience.measurable_pairOrigin line 17
3. lemma OAI.DirectionalTransience.pairOrigin_selectedBoundarySuffix line 21
4. lemma OAI.DirectionalTransience.pairOrigin_ae line 27
5. lemma OAI.DirectionalTransience.selectedBoundaryData_height line 33
6. def OAI.DirectionalTransience.commonCutObserver line 36
7. lemma OAI.DirectionalTransience.measurable_commonCutObserver line 42
8. theorem OAI.DirectionalTransience.commonCutObserver_restart line 56
9. lemma OAI.DirectionalTransience.commonCutObserver_sameHeight line 104