OAI/Probability/ParisiFinite/Time.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Time.

  1. abbrev OAI.ParisiPath.Time line 15
  2. abbrev OAI.ParisiPath.Path line 16
  3. def OAI.ParisiPath.extend line 18
  4. lemma OAI.ParisiPath.continuous_extend line 20
  5. lemma OAI.ParisiPath.extend_of_mem line 23
  6. structure OAI.ParisiPath.Drift line 27
  7. lemma OAI.ParisiPath.integrable_comp line 35
  8. def OAI.ParisiPath.next line 42
  9. lemma OAI.ParisiPath.next_apply line 47
  10. lemma OAI.ParisiPath.dist_iterate_apply line 50
  11. lemma OAI.ParisiPath.dist_iterate line 81
  12. lemma OAI.ParisiPath.exists_contracting_iterate line 94
  13. lemma OAI.ParisiPath.exists_solution line 101
  14. lemma OAI.ParisiPath.isFixedPt_iff line 108
  15. def OAI.ParisiPath.solution line 118
  16. lemma OAI.ParisiPath.solution_eq line 120
  17. lemma OAI.ParisiPath.solution_fixed line 124
  18. lemma OAI.ParisiPath.solution_unique line 128
  19. lemma OAI.ParisiPath.solution_zero line 135
  20. lemma OAI.ParisiPath.dist_next_driver line 140
  21. lemma OAI.ParisiPath.dist_next line 147
  22. def OAI.ParisiPath.amplification line 155
  23. lemma OAI.ParisiPath.dist_iterate_drivers line 159
  24. lemma OAI.ParisiPath.exists_lipschitz_solution line 174
  25. lemma OAI.ParisiPath.continuous_solution line 192
  26. lemma OAI.ParisiPath.iterate_agree_until line 196
  27. lemma OAI.ParisiPath.solution_agree_until line 213
  28. lemma OAI.ParisiPath.norm_solution_sub_driver line 231
  29. lemma OAI.ParisiPath.tendsto_iterate_solution line 240
  30. lemma OAI.ParisiPath.measurable_extend_family line 251
  31. lemma OAI.ParisiPath.measurable_next_eval line 259
  32. lemma OAI.ParisiPath.measurable_solution_eval line 271
  33. lemma OAI.ParisiPath.measurable_solution_family line 287
  34. lemma OAI.ParisiPath.aemeasurable_solution_eval line 295
  35. def OAI.ParisiPath.mesh line 308
  36. def OAI.ParisiPath.grid line 309
  37. def OAI.ParisiPath.euler line 311
  38. lemma OAI.ParisiPath.mesh_pos line 316
  39. lemma OAI.ParisiPath.grid_zero line 317
  40. lemma OAI.ParisiPath.grid_succ line 318
  41. lemma OAI.ParisiPath.grid_end line 320
  42. lemma OAI.ParisiPath.grid_mono line 323
  43. lemma OAI.ParisiPath.grid_mem line 326
  44. def OAI.ParisiPath.freeze line 330
  45. lemma OAI.ParisiPath.measurable_freeze line 332
  46. lemma OAI.ParisiPath.freeze_tendsto line 336
  47. lemma OAI.ParisiPath.freeze_on_cell line 342
  48. def OAI.ParisiPath.residual line 358
  49. def OAI.ParisiPath.totalResidual line 361
  50. lemma OAI.ParisiPath.measurable_reference line 364
  51. lemma OAI.ParisiPath.measurable_residual line 368
  52. lemma OAI.ParisiPath.residual_bound line 372
  53. lemma OAI.ParisiPath.integrable_residual line 378
  54. lemma OAI.ParisiPath.totalResidual_nonneg line 384
  55. lemma OAI.ParisiPath.totalResidual_tendsto_zero line 390
  56. lemma OAI.ParisiPath.finite_discrete_gronwall line 407
  57. lemma OAI.ParisiPath.solution_increment line 426
  58. def OAI.ParisiPath.localResidual line 437
  59. lemma OAI.ParisiPath.localResidual_nonneg line 441
  60. lemma OAI.ParisiPath.localResidual_eq_integral line 445
  61. lemma OAI.ParisiPath.sum_localResidual line 454
  62. lemma OAI.ParisiPath.euler_error_step line 461
  63. lemma OAI.ParisiPath.euler_error_bound line 505
  64. lemma OAI.ParisiPath.euler_terminal_tendsto line 530
  65. def OAI.ParisiPath.scaledDrift line 541
  66. def OAI.ParisiPath.scaledPath line 553
  67. lemma OAI.ParisiPath.extend_scaledPath line 557
  68. lemma OAI.ParisiPath.scaled_time_mem line 562
  69. lemma OAI.ParisiPath.solution_scaled line 567
  70. def OAI.ParisiPath.horizonEuler line 595
  71. lemma OAI.ParisiPath.horizonEuler_zero line 598
  72. lemma OAI.ParisiPath.horizonEuler_succ line 602
  73. lemma OAI.ParisiPath.horizonEuler_terminal_tendsto line 611
  74. lemma OAI.ParisiPath.norm_euler_sub_driver line 621
  75. lemma OAI.ParisiPath.euler_error_uniform_bound line 639
  76. lemma OAI.ParisiPath.aemeasurable_euler line 655
  77. lemma OAI.ParisiPath.aemeasurable_scaledPath_eval line 667