OAI/Probability/ProjectionMoments/BorelRules.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.NoiselessRegression.Learner.runStatusMeasurable line 14
2. instance OAI.NoiselessRegression.Learner.runStatusSingleton line 15
3. lemma OAI.NoiselessRegression.Learner.measurable_countable_select line 17
4. lemma OAI.NoiselessRegression.Learner.measurable_run line 23
5. lemma OAI.NoiselessRegression.Learner.measurable_terminal line 54
6. lemma OAI.NoiselessRegression.Learner.measurable_estimate line 59
7. lemma OAI.NoiselessRegression.Learner.admissible_of_measurable line 64
8. lemma OAI.NoiselessRegression.joint_sphere_sample_observation_quasi line 75
9. theorem OAI.NoiselessRegression.Learner.exists_borel_version line 93
10. lemma OAI.NoiselessRegression.Learner.aemeasurable_terminal_of_rules line 141
11. lemma OAI.NoiselessRegression.Learner.uniformSuccess_borel_version line 150