OAI/Probability/StrongRayleigh/IIDNoiseIncrements.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.Noise.indepFun_vectors_of_independent_pairs line 15
2. theorem OAI.Problem336AdditiveD139.Noise.indepFun_families_of_independent_pairs line 44
3. theorem OAI.Problem336AdditiveD139.Noise.indepFun_families_infinitePi line 65
4. theorem OAI.Problem336AdditiveD139.Noise.brownian_iid_shift_indep_past line 93
5. theorem OAI.Problem336AdditiveD139.Noise.brownian_iid_weighted_increment_indep_past line 110
6. theorem OAI.Problem336AdditiveD139.Noise.hasLaw_finsetSum_gaussian line 122
7. theorem OAI.Problem336AdditiveD139.Noise.hasLaw_infinitePi_eval line 141
8. theorem OAI.Problem336AdditiveD139.Noise.brownian_iid_weighted_increment_hasLaw line 147