OAI/Probability/StrongRayleigh/GroupDriftPosterior.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.groupDrift_ae_eq_condExp_of_finite_posteriors line 13
2. theorem OAI.Problem336AdditiveD139.groupDrift_ae_all_eq_condExp_of_finite_posteriors line 34
3. theorem OAI.Problem336AdditiveD139.groupDrift_ae_eq_condExp_of_observed_posteriors line 48