OAI/Probability/PosteriorReplicas/Regression/ProjectionCoupling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorRegression.matrixLabelReference line 20
2. def OAI.PosteriorRegression.projectionLaw line 23
3. def OAI.PosteriorRegression.gaussianCoupling line 27
4. def OAI.PosteriorRegression.noisyObservation line 32
5. lemma OAI.PosteriorRegression.measurable_noisyObservation line 36
6. lemma OAI.PosteriorRegression.gaussianCoupling_map_noisyObservation_zero line 41
7. lemma OAI.PosteriorRegression.gaussianCoupling_map_noisyObservation line 55
8. lemma OAI.PosteriorRegression.matrixLabelReference_outerRegular line 79
9. lemma OAI.PosteriorRegression.tendsto_noisyObservation line 86
10. theorem OAI.PosteriorRegression.projectionLaw_set_bound line 96