OAI/Probability/StrongRayleigh/GroupBrownianPosterior.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.measurable_binaryField line 19
2. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.integrable_binaryCoordinate line 24
3. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.finiteFieldMean_congr_on line 34
4. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.finiteFieldMean_zero line 46
5. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.finiteFieldMean_zero_endpoint_posterior line 52
6. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.groupDrift_ae_eq_condExp_of_endpoint_posteriors line 82
7. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.groupDrift_ae_eq_condExp_of_positive_endpoint_posteriors line 124
8. theorem OAI.Problem336AdditiveD139.GroupBrownianPosterior.groupDrift_ae_eq_condExp line 159