OAI/Probability/SpanningForest/AllPairWiener.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.AllPairWiener.Path line 14
  2. def OAI.Problem336.AllPairWiener.law line 18
  3. instance OAI.Problem336.AllPairWiener.law_isProbabilityMeasure line 21
  4. theorem OAI.Problem336.AllPairWiener.eval_hasLaw line 25
  5. theorem OAI.Problem336.AllPairWiener.isBrownian_eval line 30
  6. theorem OAI.Problem336.AllPairWiener.independent_paths line 39
  7. theorem OAI.Problem336.AllPairWiener.independent_processes line 44
  8. def OAI.Problem336.AllPairWiener.pathEval line 50
  9. theorem OAI.Problem336.AllPairWiener.measurable_pathEval line 52
  10. def OAI.Problem336.AllPairWiener.paths line 56
  11. theorem OAI.Problem336.AllPairWiener.measurable_paths line 59
  12. theorem OAI.Problem336.AllPairWiener.measurable_paths_field line 63
  13. theorem OAI.Problem336.AllPairWiener.paths_equivariant line 68
  14. theorem OAI.Problem336.AllPairWiener.paths_hasLaw line 73
  15. def OAI.Problem336.AllPairWiener.noise line 82
  16. theorem OAI.Problem336.AllPairWiener.noise_borel line 84
  17. theorem OAI.Problem336.AllPairWiener.noise_equivariant line 91
  18. theorem OAI.Problem336.AllPairWiener.continuous_noise line 95
  19. theorem OAI.Problem336.AllPairWiener.decoder_eq_nonnegative_sample line 99
  20. theorem OAI.Problem336.AllPairWiener.sampler_hasLaw_of_product line 107
  21. theorem OAI.Problem336.AllPairWiener.exists_factor_of_sampler_laws line 116