OAI/Probability/StrongRayleigh/RationalBrownian.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.RationalBrownian.sampleImage line 16
  2. lemma OAI.Problem336AdditiveD139.RationalBrownian.measurable_sampleImage line 20
  3. def OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw line 24
  4. instance OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw_isProbabilityMeasure line 27
  5. lemma OAI.Problem336AdditiveD139.RationalBrownian.sampleImage_hasLaw line 32
  6. theorem OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw_projective line 37
  7. theorem OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw_eval_hasLaw line 50
  8. theorem OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw_increment_hasLaw line 58
  9. instance OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw_isGaussian line 68
  10. lemma OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw_eval_mean line 77
  11. lemma OAI.Problem336AdditiveD139.RationalBrownian.finiteLaw_eval_covariance line 81
  12. theorem OAI.Problem336AdditiveD139.RationalBrownian.projectiveLimit_hasLaw line 88
  13. theorem OAI.Problem336AdditiveD139.RationalBrownian.projectiveLimit_isGaussianProcess line 93
  14. theorem OAI.Problem336AdditiveD139.RationalBrownian.projectiveLimit_increment_hasLaw line 98
  15. theorem OAI.Problem336AdditiveD139.RationalBrownian.projectiveLimit_eval_hasLaw line 106
  16. theorem OAI.Problem336AdditiveD139.RationalBrownian.projectiveLimit_covariance line 113
  17. theorem OAI.Problem336AdditiveD139.RationalBrownian.exists_nat_law line 125
  18. theorem OAI.Problem336AdditiveD139.RationalBrownian.exists_countable_law line 137
  19. theorem OAI.Problem336AdditiveD139.RationalBrownian.exists_countable_process line 143