OAI/Probability/StrongRayleigh/ContinuousPathLaw.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.ContinuousPathLaw.familySamples line 19
  2. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.continuous_familySamples line 22
  3. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.familySamples_injective line 27
  4. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.measurableEmbedding_familySamples line 39
  5. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.measurable_iff_dense_evaluations line 43
  6. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.measure_eq_of_dense_finiteDimensional line 50
  7. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.aemeasurable_iff_dense_evaluations line 62
  8. def OAI.Problem336AdditiveD139.ContinuousPathLaw.bundlePaths line 69
  9. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.aemeasurable_bundlePaths line 72
  10. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.bundlePaths_eval_ae_eq line 85
  11. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.exists_measurable_path_version line 92
  12. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.identDistrib_of_dense_finiteDimensional line 105
  13. def OAI.Problem336AdditiveD139.ContinuousPathLaw.rationalTime line 125
  14. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.denseRange_rationalTime line 127
  15. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.measure_eq_of_rational_finiteDimensional line 136
  16. theorem OAI.Problem336AdditiveD139.ContinuousPathLaw.measurable_iff_rational_evaluations line 143