OAI/Probability/PosteriorReplicas/Regression/StreamIntegrals.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorRegression.measurable_select line 18
2. lemma OAI.PosteriorRegression.lintegral_pi_cons line 24
3. def OAI.PosteriorRegression.streamRoute line 39
4. lemma OAI.PosteriorRegression.measurable_streamRoute line 45
5. def OAI.PosteriorRegression.continuation line 61
6. lemma OAI.PosteriorRegression.measurable_continuation line 66
7. lemma OAI.PosteriorRegression.continuation_le_one line 77
8. lemma OAI.PosteriorRegression.continuation_unroll line 84
9. def OAI.PosteriorRegression.streamFactor line 110
10. lemma OAI.PosteriorRegression.streamFactor_ne_top line 114
11. lemma OAI.PosteriorRegression.one_le_streamFactor line 118
12. lemma OAI.PosteriorRegression.PolynomialMass.mono line 124
13. lemma OAI.PosteriorRegression.continuation_mass_bound line 128
14. lemma OAI.PosteriorRegression.fin_tail_snoc line 183
15. lemma OAI.PosteriorRegression.streamRoute_snoc line 190
16. lemma OAI.PosteriorRegression.lintegral_pi_prefix line 203
17. lemma OAI.PosteriorRegression.fin_prefix_snoc line 230