OAI/Probability/SLEGauge/CutoffDrift.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactSLEGreen.cutoffDrift line 20
2. lemma OAI.ExactSLEGreen.cutoffDrift_second_bound line 23
3. lemma OAI.ExactSLEGreen.cutoffDrift_second_lipschitz line 32
4. lemma OAI.ExactSLEGreen.cutoffDrift_bound line 56
5. lemma OAI.ExactSLEGreen.cutoffDrift_lipschitz line 60
6. lemma OAI.ExactSLEGreen.cutoffDrift_eq_physical line 70
7. theorem OAI.ExactSLEGreen.state_eq_loewner_on_safe line 78
8. lemma OAI.ExactSLEHitting.firstContact_mem line 148
9. lemma OAI.ExactSLEHitting.firstContact_le_iff line 160
10. lemma OAI.ExactSLEHitting.measurable_has_contact line 178
11. lemma OAI.ExactSLEHitting.firstContact_stopping line 207
12. lemma OAI.ExactSLEHitting.boundedContact_le_iff line 223
13. lemma OAI.ExactSLEHitting.boundedContact_stopping line 242
14. lemma OAI.ExactSLEHitting.nonneg_before_boundedContact line 261
15. lemma OAI.ExactSLEHitting.boundedContact_eq_zero line 273
16. def OAI.ExactSLEGreen.physicalRadius line 288
17. lemma OAI.ExactSLEGreen.physicalRadius_continuous line 289
18. lemma OAI.ExactSLEGreen.alpha_pos line 292
19. lemma OAI.ExactSLEGreen.physicalGreen_bound line 298
20. lemma OAI.ExactSLEGreen.physicalGreen_eq_radius_sine line 318
21. lemma OAI.ExactSLEGreen.exists_localState line 334
22. def OAI.ExactSLEGreen.localState line 345
23. lemma OAI.ExactSLEGreen.localState_continuous line 347
24. lemma OAI.ExactSLEGreen.localState_adapted line 350
25. lemma OAI.ExactSLEGreen.localState_zero line 353
26. lemma OAI.ExactSLEGreen.localState_eq line 356
27. lemma OAI.ExactSLEGreen.localState_eq_zero line 360
28. theorem OAI.ExactSLEGreen.localGreen_optional line 368
29. structure OAI.ExactSLEBarrier.Evolution line 407
30. lemma OAI.ExactSLEBarrier.Evolution.logHeight_deriv line 418
31. lemma OAI.ExactSLEBarrier.Evolution.logRadius_deriv line 424
32. lemma OAI.ExactSLEBarrier.Evolution.height_le line 433