OAI/Probability/SKValue/Equations/InitialMax.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.finite_discrete_gronwall line 24
2. lemma OAI.SKValue.finite_discrete_gronwall_uniform line 53
3. lemma OAI.SKValue.driven_euler_stability line 68
4. lemma OAI.SKValue.monotone_drift_local_error line 114
5. lemma OAI.SKValue.mesh_mem_strip line 161
6. lemma OAI.SKValue.intervalIntegrable_substrip line 168
7. lemma OAI.SKValue.driven_euler_error_bound line 175
8. lemma OAI.SKValue.driven_euler_uniform_convergence line 245
9. lemma OAI.SKValue.driven_euler_uniform_bound line 293
10. def OAI.SKValue.initialMax line 348
11. lemma OAI.SKValue.initialMax_le_iff line 352
12. lemma OAI.SKValue.initialMax_lt_iff line 366
13. lemma OAI.SKValue.le_initialMax line 380
14. lemma OAI.SKValue.aestronglyMeasurable_initialMax line 383