OAI/Probability/PosteriorReplicas/Regression/StreamTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorRegression.measurePreserving_pi_prefix line 19
2. lemma OAI.PosteriorRegression.sphere_sample_observation_quasi line 29
3. lemma OAI.PosteriorRegression.streamRoute_congr line 41
4. lemma OAI.PosteriorRegression.prefix_route_cap_bound line 51