OAI/Probability/PosteriorReplicas/Learners/CompletedKernelLaw.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorRegression.map_prod_eq_bind line 10
2. def OAI.PosteriorRegression.CompletedKernelLearner.Realization.stepMap line 24
3. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.measurable_stepMap line 29
4. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.run_succ line 38
5. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.measurable_run line 46
6. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.run_depends_prefix line 62
7. def OAI.PosteriorRegression.CompletedKernelLearner.fillCoins line 75
8. lemma OAI.PosteriorRegression.CompletedKernelLearner.measurable_fillCoins line 78
9. lemma OAI.PosteriorRegression.CompletedKernelLearner.indep_fresh_coin line 85
10. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.step_law line 105
11. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.run_law line 117
12. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.measurable_terminal line 145
13. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.terminal_law line 150
14. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.measurable_estimate line 157
15. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.estimate_law line 164
16. instance OAI.PosteriorRegression.CompletedKernelLearner.estimateLaw_probability line 181