OAI/Probability/SLEGauge/PhaseStopping.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactSLEGreen.phaseActive_mem line 26
2. lemma OAI.ExactSLEGreen.phaseConstant_pos line 28
3. lemma OAI.ExactSLEGreen.phaseSigma_bound line 33
4. lemma OAI.ExactSLEGreen.physicalRegularized_pos line 37
5. lemma OAI.ExactSLEGreen.regularizedProduct_pos line 42
6. lemma OAI.ExactSLEGreen.phaseProduct_pos line 46
7. lemma OAI.ExactSLEGreen.physicalRegularized_activation line 49
8. lemma OAI.ExactSLEGreen.physicalRegularized_completion line 55
9. lemma OAI.ExactSLEGreen.physicalRegularized_midpoint line 63
10. lemma OAI.ExactSLEGreen.physicalRegularized_measurable line 71
11. lemma OAI.ExactSLEGreen.phaseProduct_measurable line 77
12. lemma OAI.ExactSLEStops.phase_mono line 87
13. lemma OAI.ExactSLEStops.boundary_eq line 94
14. def OAI.ExactSLEGreen.phaseFactor line 101
15. lemma OAI.ExactSLEGreen.phaseProduct_eq_prod line 105
16. lemma OAI.ExactSLEGreen.phaseFactor_pos line 114
17. lemma OAI.ExactSLEGreen.phaseFactor_transition line 122
18. def OAI.ExactSLEGreen.actualPhase line 172
19. lemma OAI.ExactSLEGreen.actualPhase_measurable line 176
20. lemma OAI.ExactSLEGreen.active_phase_interval line 189
21. lemma OAI.ExactSLEGreen.phase_delta_le line 201
22. lemma OAI.ExactSLEGreen.actual_phase_interval_safe line 212
23. lemma OAI.ExactSLEGreen.levelTime_clock_at_eq line 252
24. lemma OAI.ExactSLEGreen.actual_phase_transition line 258
25. lemma OAI.ExactSLEGreen.vectorState_stopped_measurable line 292
26. lemma OAI.ExactSLEGreen.regimeState_stopped_measurable line 299
27. lemma OAI.ExactSLEGreen.regularizedProduct_measurable line 307
28. lemma OAI.ExactSLEGreen.regularizedProduct_bound line 312
29. lemma OAI.ExactSLEGreen.regimeState_discount_bound line 321
30. lemma OAI.ExactSLEGreen.regularizedProduct_indicator_integrable line 332
31. theorem OAI.ExactSLEGreen.vector_regime_event_comparison line 356