OAI/Probability/StrongRayleigh/ObservationHistory.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336AdditiveD139.PosteriorLimit.endpointSpace line 16
2. def OAI.Problem336AdditiveD139.PosteriorLimit.centeredHistory line 20
3. theorem OAI.Problem336AdditiveD139.PosteriorLimit.endpointSpace_eq_comap line 23
4. theorem OAI.Problem336AdditiveD139.PosteriorLimit.observationSpace_eq_comap line 28
5. theorem OAI.Problem336AdditiveD139.PosteriorLimit.measurable_observation line 33
6. theorem OAI.Problem336AdditiveD139.PosteriorLimit.endpointSpace_le_observationSpace line 39
7. theorem OAI.Problem336AdditiveD139.PosteriorLimit.observationSpace_eq_endpoint_sup_bridge line 44
8. theorem OAI.Problem336AdditiveD139.PosteriorLimit.signal_observationSpace_eq_endpoint_sup_noise_bridge line 73