OAI/Probability/SpanningForest/ObservationPosterior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336.Observation.gaussianPDFReal_binary_shift line 12
2. theorem OAI.Problem336.Observation.gaussianPDFReal_binary_shift_prod line 26
3. def OAI.Problem336.Observation.finiteObservationFiltration line 40
4. theorem OAI.Problem336.Observation.iSup_finiteObservationFiltration line 50
5. theorem OAI.Problem336.Observation.tendsto_posterior_of_finite_stage line 61
6. theorem OAI.Problem336.Observation.limsup_posterior_of_finite_stage line 74
7. theorem OAI.Problem336.Observation.limsup_posterior_all_coordinates line 85