OAI/Probability/ParisiFinite/HorizonGrid.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Horizon Grid.

  1. def OAI.ParisiPath.horizonGrid line 17
  2. lemma OAI.ParisiPath.horizonGrid_coe line 20
  3. lemma OAI.ParisiPath.horizonGrid_mono line 23
  4. lemma OAI.ParisiPath.horizonGrid_nndist line 27
  5. def OAI.ParisiPath.standardStep line 40
  6. lemma OAI.ParisiPath.standardStep_hasLaw line 47
  7. lemma OAI.ParisiPath.standardStep_independent line 66
  8. lemma OAI.ParisiPath.standardStep_jointLaw line 71
  9. def OAI.ParisiPath.translatePath line 83
  10. lemma OAI.ParisiPath.extend_translatePath line 85
  11. lemma OAI.ParisiPath.euler_translate_step line 88
  12. lemma OAI.ParisiPath.euler_translate_bound line 111
  13. lemma OAI.ParisiPath.scaled_translatePath line 127
  14. lemma OAI.ParisiPath.horizonEuler_translate_bound line 132
  15. def OAI.ParisiPath.sourceIndex line 141
  16. lemma OAI.ParisiPath.sourceIndex_injective line 143
  17. def OAI.ParisiPath.sourceNoise line 152
  18. lemma OAI.ParisiPath.sourceNoise_jointLaw line 155
  19. def OAI.ParisiPath.initialSeed line 162
  20. lemma OAI.ParisiPath.initialSeed_aemeasurable line 165
  21. lemma OAI.ParisiPath.initialSeed_integrable_sq line 169
  22. lemma OAI.ParisiPath.initialSeed_integral_sq line 175
  23. def OAI.ParisiPath.innovationEuler line 196
  24. lemma OAI.ParisiPath.innovationEuler_measurable line 202
  25. lemma OAI.ParisiPath.innovationEuler_congr line 210
  26. def OAI.ParisiPath.pastExtension line 218
  27. lemma OAI.ParisiPath.pastExtension_measurable line 221
  28. lemma OAI.ParisiPath.innovationEuler_past line 230
  29. lemma OAI.ParisiPath.innovationEuler_independent line 236
  30. lemma OAI.ParisiPath.innovationEuler_aemeasurable line 254
  31. lemma OAI.ParisiPath.gaussian_standard_integral line 260
  32. lemma OAI.ParisiPath.gaussian_standard_integral_sq line 263
  33. lemma OAI.ParisiPath.innovationEuler_noise_mean line 270
  34. lemma OAI.ParisiPath.innovationEuler_noise_sq line 286
  35. lemma OAI.ParisiPath.cubic_taylor_bound line 313
  36. structure OAI.ParisiPath.CubicTest line 343
  37. lemma OAI.ParisiPath.CubicTest.continuous line 354
  38. lemma OAI.ParisiPath.CubicTest.continuous_d1 line 355
  39. lemma OAI.ParisiPath.CubicTest.continuous_d2 line 357
  40. lemma OAI.ParisiPath.CubicTest.lipschitz line 359
  41. def OAI.ParisiPath.thirdMomentBound line 370
  42. lemma OAI.ParisiPath.shiftedNorm_integrable_cube line 372
  43. lemma OAI.ParisiPath.shiftedNorm_integral_cube line 380
  44. lemma OAI.ParisiPath.thirdMomentBound_nonneg line 386
  45. lemma OAI.ParisiPath.scalar_euler_increment_bound line 389
  46. lemma OAI.ParisiPath.scalar_euler_increment_cube line 403
  47. lemma OAI.ParisiPath.scalar_euler_increment_thirdMoment line 413
  48. lemma OAI.ParisiPath.scalar_euler_increment_memLp line 423
  49. lemma OAI.ParisiPath.independent_gaussian_first line 440
  50. lemma OAI.ParisiPath.independent_gaussian_second line 451
  51. lemma OAI.ParisiPath.integrable_bounded_comp line 467
  52. lemma OAI.ParisiPath.weak_step_polynomial line 476
  53. lemma OAI.ParisiPath.weak_step_integrable line 533
  54. lemma OAI.ParisiPath.weak_step_integrable_polynomial line 547
  55. lemma OAI.ParisiPath.weak_step_taylor_error line 566
  56. lemma OAI.ParisiPath.weak_step_error line 595