OAI/Probability/SLEGauge/RadialBounds.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactSLEBarrier.Evolution.logRadius_le line 20
2. theorem OAI.ExactSLEBarrier.Evolution.height_barrier line 33
3. theorem OAI.ExactSLEBarrier.Evolution.time_barrier line 64
4. lemma OAI.ExactSLEGreen.localState_projection_deriv line 89
5. lemma OAI.ExactSLEGreen.Y_physicalDrift line 111
6. lemma OAI.ExactSLEGreen.J_physicalDrift line 116
7. lemma OAI.ExactSLEGreen.localState_evolution line 126
8. def OAI.ExactSLEGreen.regionMonitor line 154
9. lemma OAI.ExactSLEGreen.regionMonitor_continuous line 156
10. lemma OAI.ExactSLEGreen.regionMonitor_nonneg_iff line 160
11. lemma OAI.ExactSLEGreen.regionMonitor_nonpos_iff line 164
12. def OAI.ExactSLEGreen.regionStop line 169
13. lemma OAI.ExactSLEGreen.regionStop_stopping line 173
14. lemma OAI.ExactSLEGreen.regionStop_le line 180
15. lemma OAI.ExactSLEGreen.regionStop_safe line 184
16. lemma OAI.ExactSLEGreen.regionStop_contact line 195
17. lemma OAI.ExactSLEGreen.localState_stopped_measurable line 211
18. lemma OAI.ExactSLEGreen.regionStop_green_mean line 222
19. def OAI.ExactSLEGreen.heightFloor line 255
20. def OAI.ExactSLEGreen.logCeiling line 257
21. lemma OAI.ExactSLEGreen.heightFloor_pos line 260
22. lemma OAI.ExactSLEGreen.logCeiling_nonneg line 261
23. lemma OAI.ExactSLEGreen.heightFloor_le line 265
24. lemma OAI.ExactSLEGreen.regionStop_barriers line 279
25. lemma OAI.ExactSLEGreen.regionStop_true_exit line 349
26. lemma OAI.ExactSLEGreen.regionStop_loewner line 375
27. def OAI.ExactSLEGreen.actualState line 393
28. def OAI.ExactSLEGreen.radialTime line 395
29. def OAI.ExactSLEGreen.radialWeight line 397
30. lemma OAI.ExactSLEGreen.regionStop_actualState line 401
31. lemma OAI.ExactSLEGreen.regionStop_le_hit line 411
32. lemma OAI.ExactSLEGreen.regionStop_eq_radialTime line 425
33. lemma OAI.ExactSLEGreen.radialTime_top_of_no_hit line 438