OAI/Probability/PosteriorReplicas/Learners/CompletedKernelLearner.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PosteriorRegression.CompletedKernelLearner.Realization line 12
2. lemma OAI.PosteriorRegression.CompletedKernelLearner.exists_realization line 24
3. def OAI.PosteriorRegression.CompletedKernelLearner.realization line 31
4. abbrev OAI.PosteriorRegression.CompletedKernelLearner.Coins line 34
5. def OAI.PosteriorRegression.CompletedKernelLearner.coinsLaw line 36
6. instance OAI.PosteriorRegression.CompletedKernelLearner.coinsLaw_probability line 38
7. def OAI.PosteriorRegression.CompletedKernelLearner.Realization.toLearner line 42
8. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.transition_completed line 48
9. lemma OAI.PosteriorRegression.CompletedKernelLearner.observation_coin_quasi line 62
10. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.uniformAdmissible line 90
11. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.initial_law line 107
12. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.transition_law line 115
13. lemma OAI.PosteriorRegression.CompletedKernelLearner.Realization.output_law line 131