OAI/Probability/LogConcave/Dynamics/Curve.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LogConcaveSampling.GlobalODE.Curve line 21
2. def OAI.LogConcaveSampling.GlobalODE.extend line 23
3. lemma OAI.LogConcaveSampling.GlobalODE.extend_of_mem line 27
4. lemma OAI.LogConcaveSampling.GlobalODE.extend_continuous line 31
5. lemma OAI.LogConcaveSampling.GlobalODE.continuous_comp line 35
6. def OAI.LogConcaveSampling.GlobalODE.next line 39
7. lemma OAI.LogConcaveSampling.GlobalODE.next_apply line 46
8. lemma OAI.LogConcaveSampling.GlobalODE.iterate_dist_point line 54
9. lemma OAI.LogConcaveSampling.GlobalODE.iterate_dist line 87
10. lemma OAI.LogConcaveSampling.GlobalODE.contracting_iterate line 97
11. theorem OAI.LogConcaveSampling.GlobalODE.exists_curve line 105
12. lemma OAI.LogConcaveSampling.GlobalODE.right_deriv line 129
13. theorem OAI.LogConcaveSampling.GlobalODE.trajectory_dist_right line 138
14. lemma OAI.LogConcaveSampling.GlobalODE.left_deriv line 150
15. lemma OAI.LogConcaveSampling.GlobalODE.trajectory_unique_left line 158
16. lemma OAI.LogConcaveSampling.GlobalODE.trajectory_unique_right line 170
17. lemma OAI.LogConcaveSampling.GlobalODE.trajectory_dist_left line 190
18. lemma OAI.LogConcaveSampling.GlobalODE.trajectory_dist line 214
19. def OAI.LogConcaveSampling.GlobalODE.flow line 236
20. lemma OAI.LogConcaveSampling.GlobalODE.flow_continuous line 238
21. lemma OAI.LogConcaveSampling.GlobalODE.flow_initial line 241
22. lemma OAI.LogConcaveSampling.GlobalODE.flow_deriv line 244
23. lemma OAI.LogConcaveSampling.GlobalODE.flow_lipschitz line 248
24. lemma OAI.LogConcaveSampling.GlobalODE.flow_cocycle line 259
25. def OAI.LogConcaveSampling.GlobalODE.flowHomeomorph line 268
26. lemma OAI.LogConcaveSampling.GlobalODE.linear_field_lipschitz line 286
27. def OAI.LogConcaveSampling.GlobalODE.fundamental line 293
28. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_continuous line 296
29. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_initial line 299
30. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_deriv line 302
31. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_apply_deriv line 306
32. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_apply_initial line 311
33. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_apply_bound line 314
34. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_norm_bound line 325
35. lemma OAI.LogConcaveSampling.GlobalODE.uniform_taylor_compact line 338
36. lemma OAI.LogConcaveSampling.GlobalODE.gronwallBound_zero_linear line 374
37. def OAI.LogConcaveSampling.GlobalODE.flowSpatialCoefficient line 386
38. lemma OAI.LogConcaveSampling.GlobalODE.flowSpatialCoefficient_continuous line 391
39. lemma OAI.LogConcaveSampling.GlobalODE.flowSpatialCoefficient_bound line 397
40. def OAI.LogConcaveSampling.GlobalODE.flowLinearization line 403
41. theorem OAI.LogConcaveSampling.GlobalODE.flow_hasFDerivAt_left line 409
42. lemma OAI.LogConcaveSampling.GlobalODE.flow_differentiable_left line 481
43. lemma OAI.LogConcaveSampling.GlobalODE.flow_joint_continuous line 493
44. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_difference_bound line 511
45. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_parameter_continuous line 562
46. lemma OAI.LogConcaveSampling.GlobalODE.flowLinearization_continuous_initial line 601
47. lemma OAI.LogConcaveSampling.GlobalODE.flow_contDiff_one_left line 611
48. lemma OAI.LogConcaveSampling.GlobalODE.fundamental_cocycle line 625
49. def OAI.LogConcaveSampling.GlobalODE.fundamentalEquiv line 637
50. lemma OAI.LogConcaveSampling.GlobalODE.flow_contDiff_one_to_left line 664
51. theorem OAI.LogConcaveSampling.GlobalODE.flow_contDiff_one line 676