OAI/Probability/GaussianReplacement/Sampling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CurrentProjection.StreamKernel.CompletedLearner.Sampling line 16
2. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.exists_sampling line 27
3. def OAI.CurrentProjection.StreamKernel.CompletedLearner.sampling line 36
4. def OAI.CurrentProjection.StreamKernel.CompletedLearner.coinIndex line 40
5. def OAI.CurrentProjection.StreamKernel.CompletedLearner.Sampling.program line 42
6. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.Sampling.measurable_initialChoice line 47
7. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.Sampling.measurable_program_transition line 50
8. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.Sampling.measurable_program_output line 57
9. lemma OAI.CurrentProjection.StreamKernel.measurable_program_run line 74
10. lemma OAI.CurrentProjection.StreamKernel.measurable_program_estimate line 110
11. lemma OAI.CurrentProjection.StreamKernel.admissible_of_borel line 117
12. lemma OAI.CurrentProjection.StreamKernel.CompletedLearner.Sampling.admissible line 131