OAI/Probability/StrongRayleigh/PosteriorLimit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.PosteriorLimit.tendsto_of_ae_eq_condExp line 16
2. theorem OAI.Problem336AdditiveD139.PosteriorLimit.limsup_ae_eq_condExp line 26
3. theorem OAI.Problem336AdditiveD139.PosteriorLimit.tendsto_eLpNorm_of_ae_eq_condExp line 34
4. def OAI.Problem336AdditiveD139.PosteriorLimit.observationSpace line 49
5. theorem OAI.Problem336AdditiveD139.PosteriorLimit.observationSpace_mono line 52
6. theorem OAI.Problem336AdditiveD139.PosteriorLimit.observationSpace_le line 58
7. theorem OAI.Problem336AdditiveD139.PosteriorLimit.iSup_observationSpace_eq line 63
8. def OAI.Problem336AdditiveD139.PosteriorLimit.observationFiltration line 72
9. theorem OAI.Problem336AdditiveD139.PosteriorLimit.limsup_ae_eq_full_observation_condExp line 79