OAI/Probability/ProjectionMoments/StoppingKernel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.capWeight_mass_mixed line 15
2. lemma OAI.NoiselessRegression.continuation_mixed_integral_bound line 49
3. lemma OAI.NoiselessRegression.route_mixed_bound line 69
4. def OAI.NoiselessRegression.Learner.haltShift line 116
5. def OAI.NoiselessRegression.Learner.haltRoute line 120
6. lemma OAI.NoiselessRegression.Learner.measurable_haltRoute line 128
7. def OAI.NoiselessRegression.Learner.haltChild line 148
8. def OAI.NoiselessRegression.Learner.stoppedContinuation line 153
9. lemma OAI.NoiselessRegression.Learner.measurable_stoppedContinuation line 159
10. lemma OAI.NoiselessRegression.Learner.stoppedContinuation_le_one line 178
11. lemma OAI.NoiselessRegression.Learner.stoppedContinuation_unroll line 192
12. lemma OAI.NoiselessRegression.Learner.stoppedContinuation_mass_bound line 228
13. def OAI.NoiselessRegression.Learner.taggedWeight line 310
14. lemma OAI.NoiselessRegression.Learner.measurable_taggedWeight line 314
15. lemma OAI.NoiselessRegression.Learner.continuation_tagged_eq line 318
16. lemma OAI.NoiselessRegression.Learner.tagged_continuation_mass line 340
17. lemma OAI.NoiselessRegression.Learner.stopped_route_mixed_bound line 369