OAI/Probability/ParisiFinite/Model.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Model.

  1. lemma OAI.BrownianConstruction.l2_mean_inner line 26
  2. lemma OAI.BrownianConstruction.l2_square_integral line 34
  3. lemma OAI.BrownianConstruction.l2_variance line 40
  4. lemma OAI.BrownianConstruction.continuous_l2_mean line 45
  5. lemma OAI.BrownianConstruction.continuous_l2_variance line 49
  6. lemma OAI.BrownianConstruction.hasGaussianLaw_l2_limit line 53
  7. lemma OAI.BrownianConstruction.isClosed_gaussian_l2 line 77
  8. def OAI.BrownianConstruction.gaussianProduct line 91
  9. instance OAI.BrownianConstruction.(instance at line 92) line 92
  10. lemma OAI.BrownianConstruction.gaussianCoordinate_law line 95
  11. lemma OAI.BrownianConstruction.gaussianCoordinate_gaussian line 98
  12. lemma OAI.BrownianConstruction.gaussianCoordinate_memLp line 101
  13. def OAI.BrownianConstruction.gaussianCoordinate line 104
  14. lemma OAI.BrownianConstruction.gaussianCoordinate_ae line 106
  15. lemma OAI.BrownianConstruction.gaussianCoordinate_mean line 108
  16. lemma OAI.BrownianConstruction.gaussianCoordinates_independent line 111
  17. lemma OAI.BrownianConstruction.gaussianCoordinate_variance line 115
  18. lemma OAI.BrownianConstruction.gaussianCoordinate_inner line 119
  19. lemma OAI.BrownianConstruction.gaussianCoordinates_orthonormal line 146
  20. def OAI.BrownianConstruction.gaussianLpIsometry line 150
  21. lemma OAI.BrownianConstruction.hasSum_gaussianLpIsometry line 153
  22. lemma OAI.BrownianConstruction.gaussianCoordinates_sum_ae line 157
  23. lemma OAI.BrownianConstruction.gaussianCoordinates_sum_gaussian line 172
  24. lemma OAI.BrownianConstruction.gaussianLpIsometry_gaussian line 187
  25. lemma OAI.BrownianConstruction.gaussianLpIsometry_mean line 192
  26. def OAI.BrownianConstruction.gaussianHilbertMap line 216
  27. lemma OAI.BrownianConstruction.gaussianHilbertMap_gaussian line 218
  28. lemma OAI.BrownianConstruction.gaussianHilbertMap_mean line 221
  29. lemma OAI.BrownianConstruction.linear_apply_pi line 225
  30. lemma OAI.BrownianConstruction.gaussianHilbertMap_sum_ae line 235
  31. lemma OAI.BrownianConstruction.gaussianHilbertMap_joint_gaussian line 251
  32. lemma OAI.BrownianConstruction.gaussianHilbertMap_covariance line 268
  33. def OAI.BrownianConstruction.initialIndicator line 288
  34. lemma OAI.BrownianConstruction.initialIndicator_inner line 291
  35. def OAI.BrownianConstruction.preBrownian line 298
  36. lemma OAI.BrownianConstruction.preBrownian_gaussian line 300
  37. lemma OAI.BrownianConstruction.preBrownian_mean line 302
  38. lemma OAI.BrownianConstruction.preBrownian_covariance line 304
  39. lemma OAI.BrownianConstruction.preBrownian_isPreBrownian line 307
  40. def OAI.BrownianConstruction.gaussianFourth line 320
  41. lemma OAI.BrownianConstruction.gaussianFourth_nonneg line 321
  42. lemma OAI.BrownianConstruction.gaussian_abs_fourth_integrable line 322
  43. lemma OAI.BrownianConstruction.gaussian_abs_fourth line 325
  44. lemma OAI.BrownianConstruction.fourth_tail_bound line 340
  45. def OAI.BrownianConstruction.dyadicPoint line 372
  46. def OAI.BrownianConstruction.dyadicIndex line 373
  47. def OAI.BrownianConstruction.dyadicRound line 374
  48. lemma OAI.BrownianConstruction.dyadicPoint_mono line 376
  49. lemma OAI.BrownianConstruction.dyadicPoint_succ line 379
  50. lemma OAI.BrownianConstruction.dyadicRound_le line 385
  51. lemma OAI.BrownianConstruction.lt_dyadicRound_add line 388
  52. lemma OAI.BrownianConstruction.dyadicIndex_le line 393
  53. lemma OAI.BrownianConstruction.dyadicIndex_succ_div line 397
  54. lemma OAI.BrownianConstruction.dyadicPoint_double line 401
  55. lemma OAI.BrownianConstruction.dyadicRound_successor_cases line 408
  56. def OAI.BrownianConstruction.DyadicGood line 428
  57. lemma OAI.BrownianConstruction.round_step_bound line 432
  58. lemma OAI.BrownianConstruction.dyadicRound_cauchy line 448
  59. def OAI.BrownianConstruction.dyadicLimit line 460
  60. lemma OAI.BrownianConstruction.tendsto_dyadicLimit line 461
  61. lemma OAI.BrownianConstruction.dyadicLimit_error line 466
  62. lemma OAI.BrownianConstruction.dyadic_increment_tail line 494
  63. def OAI.BrownianConstruction.dyadicBad line 507
  64. lemma OAI.BrownianConstruction.dyadicBad_measure line 510
  65. lemma OAI.BrownianConstruction.ae_dyadicGood line 537
  66. lemma OAI.BrownianConstruction.dyadicIndex_neighbors line 562
  67. lemma OAI.BrownianConstruction.nearby_round_bound line 585
  68. lemma OAI.BrownianConstruction.continuous_dyadicLimit line 604