OAI/Probability/ProjectionMoments/Stopping.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.continuation_mass_bound_ceil line 16
2. lemma OAI.NoiselessRegression.continuation_cap_integral_bound_ceil line 79
3. lemma OAI.NoiselessRegression.route_cap_bound_ceil line 93
4. instance OAI.NoiselessRegression.Learner.taggedMeasurableSingletonClass line 138
5. lemma OAI.NoiselessRegression.Learner.card_taggedState line 141
6. def OAI.NoiselessRegression.Learner.decodeTagged line 145
7. def OAI.NoiselessRegression.Learner.taggedStep line 149
8. lemma OAI.NoiselessRegression.Learner.measurable_taggedStep line 158
9. def OAI.NoiselessRegression.Learner.taggedOutput line 171
10. lemma OAI.NoiselessRegression.Learner.decode_taggedStart line 175
11. lemma OAI.NoiselessRegression.Learner.run_eq_taggedRoute line 179
12. lemma OAI.NoiselessRegression.Learner.estimate_eq_taggedRoute line 199
13. lemma OAI.NoiselessRegression.Learner.taggedStep_congr line 214
14. lemma OAI.NoiselessRegression.Learner.frozen_success_bound_tagged line 222
15. lemma OAI.NoiselessRegression.Learner.streaming_success_bound_tagged line 260