OAI/Probability/FreeIsing/Stochastic/WienerSampler.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.WienerSampler.Path line 13
  2. instance OAI.Problem367.WienerSampler.pathMeasurableSpace line 15
  3. instance OAI.Problem367.WienerSampler.pathBorelSpace line 16
  4. theorem OAI.Problem367.WienerSampler.measurableEmbedding_denseEval line 18
  5. theorem OAI.Problem367.WienerSampler.measurable_path_of_eval line 26
  6. theorem OAI.Problem367.WienerSampler.exists_measurable_path_version line 31
  7. theorem OAI.Problem367.WienerSampler.measurable_brownian_version line 54
  8. theorem OAI.Problem367.WienerSampler.isBrownian_eval_map line 59
  9. theorem OAI.Problem367.WienerSampler.exists_wienerMeasure line 76
  10. def OAI.Problem367.WienerSampler.wienerMeasure line 89
  11. instance OAI.Problem367.WienerSampler.wienerProbability line 91
  12. theorem OAI.Problem367.WienerSampler.coordinate_isBrownianReal line 94
  13. theorem OAI.Problem367.WienerSampler.exists_uniform01_wiener_sampler line 98
  14. theorem OAI.Problem367.WienerSampler.isBrownianReal_of_sampler line 102
  15. def OAI.Problem367.WienerSampler.sample line 108
  16. theorem OAI.Problem367.WienerSampler.measurable_sample line 110
  17. theorem OAI.Problem367.WienerSampler.map_sample line 113
  18. theorem OAI.Problem367.WienerSampler.sample_isBrownianReal line 116
  19. theorem OAI.Problem367.WienerSampler.measurable_sample_eval line 119
  20. theorem OAI.Problem367.WienerSampler.wiener_starts_zero line 124
  21. def OAI.Problem367.WienerSampler.array line 127
  22. theorem OAI.Problem367.WienerSampler.measurable_array line 130
  23. theorem OAI.Problem367.WienerSampler.map_array line 133
  24. theorem OAI.Problem367.WienerSampler.array_relabel line 138
  25. theorem OAI.Problem367.WienerSampler.array_iIndepFun line 141
  26. theorem OAI.Problem367.WienerSampler.array_isBrownianReal line 145