OAI/Probability/ProjectionMoments/Kernels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.finite_kernel_borel_version line 12
2. structure OAI.NoiselessRegression.FiniteKernelLearner.BorelRules line 46
3. lemma OAI.NoiselessRegression.FiniteKernelLearner.exists_borel_version line 49
4. def OAI.NoiselessRegression.coinRun line 65
5. lemma OAI.NoiselessRegression.measurable_coinRun line 71
6. lemma OAI.NoiselessRegression.lintegral_coinRun line 86
7. lemma OAI.NoiselessRegression.coinRun_law line 107
8. lemma OAI.NoiselessRegression.kernelRun_congr line 119