OAI/Probability/ParisiFinite/InnovationEulerMemLp.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Innovation Euler Mem Lp.

  1. lemma OAI.ParisiPath.innovationEuler_memLp line 20
  2. lemma OAI.ParisiPath.CubicTest.integrable_comp line 34
  3. def OAI.ParisiPath.generator line 46
  4. lemma OAI.ParisiPath.generator_bound line 49
  5. lemma OAI.ParisiPath.mesh_le_one line 59
  6. lemma OAI.ParisiPath.innovationEuler_generator_step line 64
  7. lemma OAI.ParisiPath.innovationEuler_generator_sum line 87
  8. def OAI.ParisiPath.frozenEuler line 119
  9. lemma OAI.ParisiPath.freeze_index_le line 122
  10. lemma OAI.ParisiPath.frozenEuler_tendsto line 128
  11. lemma OAI.ParisiPath.reference_ae_continuous_of_joint line 143
  12. def OAI.ParisiPath.brownianPath line 156
  13. lemma OAI.ParisiPath.brownianPath_eq_ae line 159
  14. lemma OAI.ParisiPath.brownianPath_aemeasurable_eval line 167
  15. lemma OAI.ParisiPath.innovationEuler_eq_euler line 172
  16. lemma OAI.ParisiPath.brownian_solution_integrable line 198
  17. lemma OAI.ParisiPath.generator_aemeasurable line 212
  18. lemma OAI.ParisiPath.generator_frozen_aemeasurable line 220
  19. def OAI.ParisiPath.expectedFrozenGenerator line 230
  20. def OAI.ParisiPath.expectedGenerator line 234
  21. lemma OAI.ParisiPath.expectedFrozenGenerator_measurable line 238
  22. lemma OAI.ParisiPath.expectedGenerator_bound line 243
  23. lemma OAI.ParisiPath.expectedFrozenGenerator_bound line 249
  24. lemma OAI.ParisiPath.expectedFrozenGenerator_tendsto line 255
  25. lemma OAI.ParisiPath.expectedFrozenGenerator_intervalIntegrable line 280
  26. lemma OAI.ParisiPath.expectedFrozenGenerator_integral_tendsto line 287
  27. lemma OAI.ParisiPath.freeze_index_on_cell line 302
  28. lemma OAI.ParisiPath.expectedFrozenGenerator_cell_integral line 308
  29. lemma OAI.ParisiPath.expectedFrozenGenerator_integral_eq_sum line 324
  30. lemma OAI.ParisiPath.brownianEuler_weak_error line 334
  31. lemma OAI.ParisiPath.brownianEuler_integrable line 359
  32. lemma OAI.ParisiPath.brownianEuler_expected_test_tendsto line 366
  33. lemma OAI.ParisiPath.mesh_tendsto_zero line 394
  34. theorem OAI.ParisiPath.brownian_solution_generator_identity line 401
  35. structure OAI.ParisiPath.QuadraticTest line 423
  36. lemma OAI.ParisiPath.QuadraticTest.continuous line 436
  37. lemma OAI.ParisiPath.QuadraticTest.continuous_d1 line 438
  38. lemma OAI.ParisiPath.QuadraticTest.lipschitz line 440
  39. def OAI.ParisiPath.smoothConvolution line 447
  40. lemma OAI.ParisiPath.smoothConvolution_eq line 450
  41. lemma OAI.ParisiPath.smoothConvolution_integrable line 453
  42. lemma OAI.ParisiPath.hasDerivAt_smoothConvolution line 458
  43. lemma OAI.ParisiPath.smoothConvolution_bound line 481
  44. lemma OAI.ParisiPath.smoothConvolution_smooth line 496
  45. lemma OAI.ParisiPath.smoothConvolution_d1 line 501
  46. lemma OAI.ParisiPath.smoothConvolution_d2 line 506
  47. lemma OAI.ParisiPath.smoothConvolution_d3 line 512
  48. lemma OAI.ParisiPath.smoothConvolution_d3_bound line 520
  49. def OAI.ParisiPath.QuadraticTest.mollify line 540
  50. def OAI.ParisiPath.shrinkingBump line 553
  51. lemma OAI.ParisiPath.shrinkingBump_tendsto line 561
  52. lemma OAI.ParisiPath.smoothConvolution_tendsto line 565
  53. lemma OAI.ParisiPath.smoothConvolution_error line 569
  54. lemma OAI.ParisiPath.QuadraticTest.integrable_comp line 583
  55. lemma OAI.ParisiPath.mollify_expected_test_tendsto line 594
  56. lemma OAI.ParisiPath.expectedGenerator_aestronglyMeasurable line 608
  57. def OAI.ParisiPath.generatorC2 line 619
  58. def OAI.ParisiPath.expectedGeneratorC2 line 622
  59. lemma OAI.ParisiPath.mollify_generator_tendsto line 626
  60. lemma OAI.ParisiPath.mollify_expectedGenerator_tendsto line 633
  61. lemma OAI.ParisiPath.mollify_generator_integral_tendsto line 643
  62. theorem OAI.ParisiPath.brownian_solution_generator_identity_C2 line 659