OAI/Probability/StrongRayleigh/BrownianPathLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.preBrownian_finite_eval_identDistrib line 20
  2. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.preBrownian_rational_identDistrib line 31
  3. def OAI.Problem336AdditiveD139.ContinuousPathLaw.rationalSamples line 53
  4. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.measurableEmbedding_rationalSamples line 55
  5. def OAI.Problem336AdditiveD139.ContinuousPathLaw.brownianPath line 62
  6. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.brownianPath_samples_ae_eq line 70
  7. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.aemeasurable_brownianPath line 78
  8. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.brownianPath_identDistrib line 84
  9. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.iIndepFun_paths_iff_rationalSamples line 96
  10. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.iIndepFun_brownianPath line 110
  11. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.map_brownianPath_family_eq_infinitePi line 117