OAI/Probability/SLEGauge/RadialRestart.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.LoewnerRestart.physicalRadius_actual_eq_inv_deriv line 18
2. lemma OAI.SLEExactGauge.LoewnerRestart.radialTime_restart line 27
3. lemma OAI.SLEExactGauge.LoewnerRestart.radialTime_restart_top_iff line 79
4. lemma OAI.SLEExactGauge.LoewnerRestart.radialWeight_restart line 90
5. lemma OAI.ExactSLEGreen.actualState_continuousOn line 144
6. lemma OAI.ExactSLEGreen.actualState_bounded_until line 175
7. def OAI.ExactSLEGreen.exhaustionHeight line 193
8. lemma OAI.ExactSLEGreen.exhaustionHeight_pos line 196
9. lemma OAI.ExactSLEGreen.exhaustionHeight_le line 199
10. lemma OAI.ExactSLEGreen.exhaustionHeight_tendsto line 202
11. def OAI.ExactSLEGreen.exhaustionNorm line 210
12. def OAI.ExactSLEGreen.exhaustionStop line 213
13. lemma OAI.ExactSLEGreen.exhaustionRegion_initial line 217
14. lemma OAI.ExactSLEGreen.exhaustionStop_stopping line 229
15. lemma OAI.ExactSLEGreen.exhaustionStop_le line 233
16. lemma OAI.ExactSLEGreen.exhaustionStop_agrees line 236
17. lemma OAI.ExactSLEGreen.exhaustionStop_eventually line 244
18. lemma OAI.ExactSLEGreen.exhaustionStop_measurable line 277
19. def OAI.ExactSLEGreen.killedObservable line 286
20. def OAI.ExactSLEGreen.localizedObservable line 290
21. lemma OAI.ExactSLEGreen.localizedObservable_joint_measurable line 295
22. lemma OAI.ExactSLEGreen.localizedObservable_tendsto line 304
23. lemma OAI.ExactSLEGreen.killedObservable_joint_measurable line 317
24. lemma OAI.ExactSLEGreen.killedObservable_nonneg line 323
25. lemma OAI.ExactSLEGreen.greenLifetime_measurable line 337
26. lemma OAI.ExactSLEGreen.lifetimeCost_measurable line 342
27. theorem OAI.ExactSLEGreen.global_lifetime_test_budget line 348
28. lemma OAI.ExactSLEGreen.localizedObservable_occupation line 398
29. theorem OAI.ExactSLEGreen.global_lifetime_occupation_budget line 417