OAI/Probability/FirstPassage/CrossingTilt.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.crossingEvent line 12
2. theorem OAI.PlanarFPP.measurableSet_crossingEvent line 17
3. theorem OAI.PlanarFPP.crossingEvent_depends line 20
4. theorem OAI.PlanarFPP.crossingEvent_tilt_implication line 24
5. theorem OAI.PlanarFPP.source_tilt_exponent_bound line 55
6. theorem OAI.PlanarFPP.exponential_crossing_tilt_bound line 66