OAI/Probability/SKValue/Evolution/TimePatch.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.patchTime line 11
2. lemma OAI.SKValue.patchTime_left line 14
3. lemma OAI.SKValue.patchTime_right line 16
4. lemma OAI.SKValue.patchTime_continuous line 19
5. lemma OAI.SKValue.patchTime_bound line 42
6. lemma OAI.SKValue.patchTime_lipschitz line 52
7. lemma OAI.SKValue.patchTime_intervalIntegrable line 83
8. lemma OAI.SKValue.patchTime_integral_left line 99
9. lemma OAI.SKValue.patchTime_integral_right line 105
10. lemma OAI.SKValue.patchTime_primitive line 113