OAI/Probability/SKBarriers/Dynamics/Crossing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.lastCrossing line 13
2. theorem OAI.SK.Analytic.lastCrossing_le line 16
3. theorem OAI.SK.Analytic.lastCrossing_spec line 19
4. theorem OAI.SK.Analytic.lastCrossing_after line 24
5. theorem OAI.SK.Analytic.lastCrossing_band line 28
6. theorem OAI.SK.Analytic.lastCrossing_search line 39
7. theorem OAI.SK.Analytic.lastCrossing_zero_of_none line 51
8. theorem OAI.SK.Analytic.anchored_backwards_crossing line 57
9. def OAI.SK.Analytic.firstCrossing line 80
10. theorem OAI.SK.Analytic.firstCrossing_band line 83