OAI/Probability/ParisiFinite/ScaledTimeMem.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Scaled Time Mem.

  1. lemma OAI.ParisiPath.scaledTime_mem line 17
  2. def OAI.ParisiPath.rescalePath line 22
  3. lemma OAI.ParisiPath.extend_rescalePath line 27
  4. def OAI.ParisiPath.Drift.rescale line 33
  5. lemma OAI.ParisiPath.solution_rescale line 52
  6. lemma OAI.ParisiPath.Drift.rescale_joint line 82
  7. lemma OAI.ParisiPath.brownianPath_rescale line 97
  8. lemma OAI.ParisiPath.brownian_solution_rescale line 106
  9. def OAI.ParisiPath.TimeQuadraticTest.rescale line 129
  10. lemma OAI.ParisiPath.brownian_solution_rescale_extend line 188
  11. lemma OAI.ParisiPath.timeGeneratorC2_rescale line 199
  12. lemma OAI.ParisiPath.timeDerivativeC2_rescale line 222
  13. theorem OAI.ParisiPath.brownian_solution_time_generator_at line 234
  14. def OAI.ParisiFinite.finiteSquareKernel line 289
  15. lemma OAI.ParisiFinite.finiteSquareKernel_bound line 295
  16. lemma OAI.ParisiFinite.finiteSquareKernel_integrable line 315
  17. lemma OAI.ParisiFinite.expected_finiteSquareKernel_eq line 333
  18. lemma OAI.ParisiFinite.expected_finiteSquareKernel_aestronglyMeasurable line 350
  19. lemma OAI.ParisiFinite.expected_finiteSquareKernel_bound line 364
  20. theorem OAI.ParisiFinite.finite_schedule_square_verification line 373
  21. def OAI.ParisiFinite.squareKernel line 411
  22. lemma OAI.ParisiFinite.global_dyadic_squareKernel_tendsto line 416
  23. lemma OAI.ParisiFinite.expected_global_dyadic_squareKernel_tendsto line 429
  24. lemma OAI.ParisiFinite.expected_global_dyadic_gradient_square_tendsto line 445
  25. theorem OAI.ParisiFinite.canonical_square_verification line 472
  26. def OAI.ParisiFinite.finiteVerificationKernel line 532
  27. def OAI.ParisiFinite.verificationKernel line 537
  28. lemma OAI.ParisiFinite.finiteVerificationKernel_bound line 542
  29. lemma OAI.ParisiFinite.finiteVerificationKernel_integrable line 565
  30. lemma OAI.ParisiFinite.expected_finiteVerificationKernel_eq line 579
  31. lemma OAI.ParisiFinite.expected_finiteVerificationKernel_aestronglyMeasurable line 595
  32. lemma OAI.ParisiFinite.expected_finiteVerificationKernel_bound line 609
  33. lemma OAI.ParisiFinite.global_dyadic_verificationKernel_tendsto line 617
  34. lemma OAI.ParisiFinite.expected_global_dyadic_verificationKernel_tendsto line 629
  35. theorem OAI.ParisiFinite.canonical_verification line 646