OAI/Probability/ParisiFinite/TimeCubicTest.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Time Cubic Test.

  1. structure OAI.ParisiPath.TimeCubicTest line 23
  2. def OAI.ParisiPath.TimeCubicTest.slice line 44
  3. lemma OAI.ParisiPath.expected_kernel_measurable line 54
  4. lemma OAI.ParisiPath.expected_kernel_interval_swap line 65
  5. def OAI.ParisiPath.timeFrozenGenerator line 95
  6. def OAI.ParisiPath.timeGenerator line 99
  7. def OAI.ParisiPath.timeFrozenDerivative line 104
  8. def OAI.ParisiPath.timeDerivative line 108
  9. lemma OAI.ParisiPath.timeFrozenGenerator_measurable line 112
  10. lemma OAI.ParisiPath.timeFrozenGenerator_bound line 117
  11. lemma OAI.ParisiPath.timeFrozenDerivative_measurable line 122
  12. lemma OAI.ParisiPath.timeFrozenDerivative_bound line 133
  13. lemma OAI.ParisiPath.timeFrozenGenerator_tendsto line 138
  14. lemma OAI.ParisiPath.nextFrozenEuler_tendsto line 156
  15. lemma OAI.ParisiPath.timeFrozenDerivative_tendsto line 177
  16. lemma OAI.ParisiPath.timeFrozenGenerator_intervalIntegrable line 191
  17. lemma OAI.ParisiPath.timeFrozenDerivative_intervalIntegrable line 198
  18. lemma OAI.ParisiPath.timeFrozenGenerator_integral_tendsto line 205
  19. lemma OAI.ParisiPath.timeFrozenDerivative_integral_tendsto line 219
  20. lemma OAI.ParisiPath.brownianEuler_integrable_at line 241
  21. lemma OAI.ParisiPath.brownianEuler_generator_step line 248
  22. lemma OAI.ParisiPath.timeFrozenGenerator_cell_integral line 265
  23. lemma OAI.ParisiPath.timeFrozenDerivative_cell_integral line 283
  24. lemma OAI.ParisiPath.timeEuler_weak_step line 311
  25. lemma OAI.ParisiPath.timeEuler_weak_error line 325
  26. theorem OAI.ParisiPath.brownian_solution_time_generator_identity line 371
  27. structure OAI.ParisiPath.TimeQuadraticTest line 397
  28. def OAI.ParisiPath.TimeQuadraticTest.slice line 418
  29. lemma OAI.ParisiPath.smoothConvolution_joint_continuousAt line 430
  30. lemma OAI.ParisiPath.smoothConvolution_joint_measurable line 450
  31. lemma OAI.ParisiPath.smoothConvolution_time_integral line 459
  32. def OAI.ParisiPath.TimeQuadraticTest.mollify line 494
  33. lemma OAI.ParisiPath.timeGenerator_aestronglyMeasurable line 534
  34. lemma OAI.ParisiPath.timeDerivative_aestronglyMeasurable line 544
  35. lemma OAI.ParisiPath.timeDerivative_bound line 554
  36. def OAI.ParisiPath.timeGeneratorC2 line 559
  37. def OAI.ParisiPath.timeDerivativeC2 line 563
  38. lemma OAI.ParisiPath.mollify_timeGenerator_tendsto line 567
  39. lemma OAI.ParisiPath.mollify_timeDerivative_tendsto line 573
  40. lemma OAI.ParisiPath.mollify_timeGenerator_integral_tendsto line 585
  41. lemma OAI.ParisiPath.mollify_timeDerivative_integral_tendsto line 599
  42. theorem OAI.ParisiPath.brownian_solution_time_generator_identity_C2 line 614