OAI/Probability/Subsphere/Regression/Streaming.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereRegression.measurable_select line 20
2. lemma OAI.SubsphereRegression.lintegral_pi_cons line 26
3. def OAI.SubsphereRegression.streamRoute line 41
4. lemma OAI.SubsphereRegression.measurable_streamRoute line 47
5. def OAI.SubsphereRegression.continuation line 63
6. lemma OAI.SubsphereRegression.measurable_continuation line 68
7. lemma OAI.SubsphereRegression.continuation_le_one line 79
8. lemma OAI.SubsphereRegression.continuation_unroll line 86
9. def OAI.SubsphereRegression.streamFactor line 112
10. lemma OAI.SubsphereRegression.streamFactor_ne_top line 116
11. lemma OAI.SubsphereRegression.one_le_streamFactor line 120
12. lemma OAI.SubsphereRegression.PolynomialMass.mono line 126
13. lemma OAI.SubsphereRegression.continuation_mass_bound line 130
14. lemma OAI.SubsphereRegression.fin_tail_snoc line 185
15. lemma OAI.SubsphereRegression.streamRoute_snoc line 192
16. lemma OAI.SubsphereRegression.lintegral_pi_prefix line 205
17. lemma OAI.SubsphereRegression.fin_prefix_snoc line 232
18. def OAI.SubsphereRegression.Learner.forcedRun line 245
19. lemma OAI.SubsphereRegression.Learner.forcedRun_eq_route line 252
20. lemma OAI.SubsphereRegression.Learner.run_forced_witness line 264
21. lemma OAI.SubsphereRegression.Learner.terminal_forced_witness line 285
22. def OAI.SubsphereRegression.capWeight line 298
23. lemma OAI.SubsphereRegression.measurable_capWeight line 302
24. lemma OAI.SubsphereRegression.capWeight_le_one line 306
25. lemma OAI.SubsphereRegression.capWeight_mass line 311
26. lemma OAI.SubsphereRegression.ambient_mass_bound line 319
27. lemma OAI.SubsphereRegression.continuation_cap_integral_bound line 330
28. lemma OAI.SubsphereRegression.route_cap_bound line 344
29. lemma OAI.SubsphereRegression.projectionLaw_absolutelyContinuous line 389
30. lemma OAI.SubsphereRegression.sphere_observation_quasi line 415