OAI/Probability/StrongRayleigh/BrownianKolmogorov.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.BrownianConstruction.integral_pow_four_gaussianReal line 14
2. theorem OAI.Problem336AdditiveD139.BrownianConstruction.integral_abs_pow_four_of_hasLaw line 60
3. theorem OAI.Problem336AdditiveD139.BrownianConstruction.integrable_abs_pow_four_of_hasLaw line 69
4. theorem OAI.Problem336AdditiveD139.BrownianConstruction.lintegral_edist_pow_four_of_increment_law line 76
5. theorem OAI.Problem336AdditiveD139.BrownianConstruction.preBrownian_integral_abs_sub_pow_four line 88
6. theorem OAI.Problem336AdditiveD139.BrownianConstruction.isKolmogorovProcess_of_gaussian_increments line 94
7. theorem OAI.Problem336AdditiveD139.BrownianConstruction.isAEKolmogorovProcess_of_gaussian_increments line 107
8. theorem OAI.Problem336AdditiveD139.BrownianConstruction.preBrownian_isAEKolmogorovProcess line 121