OAI/Probability/ProjectionMoments/Realization.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.NoiselessRegression.FiniteKernelLearner.Realizer line 14
2. lemma OAI.NoiselessRegression.FiniteKernelLearner.exists_realizer line 22
3. def OAI.NoiselessRegression.FiniteKernelLearner.tapeLaw line 39
4. instance OAI.NoiselessRegression.FiniteKernelLearner.tapeLaw_probability line 42
5. def OAI.NoiselessRegression.FiniteKernelLearner.Realizer.toLearner line 47
6. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.measurableRules line 53
7. def OAI.NoiselessRegression.FiniteKernelLearner.Realizer.taggedTransition line 62
8. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.tagged_measurable line 67
9. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.tagged_law line 78
10. def OAI.NoiselessRegression.FiniteKernelLearner.Realizer.terminalOutput line 94
11. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.terminalOutput_measurable line 99
12. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.terminalOutput_law line 105
13. def OAI.NoiselessRegression.FiniteKernelLearner.experimentLaw line 111
14. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.run_eq_coinRun line 114
15. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.estimate_eq_coinRun line 137
16. lemma OAI.NoiselessRegression.map_finite_prod_eq_bind line 150
17. lemma OAI.NoiselessRegression.coinRun_output_law line 162
18. def OAI.NoiselessRegression.FiniteKernelLearner.Realizer.terminalJointOutput line 188
19. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.terminalJointOutput_measurable line 191
20. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.terminalJointOutput_law line 195
21. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.terminal_eq_coinRun line 201
22. theorem OAI.NoiselessRegression.FiniteKernelLearner.Realizer.conditional_joint_law line 212