OAI/Probability/SpanningForest/PicardSamplerLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.PicardSampler.decodedIntegers line 13
2. def OAI.Problem336.PicardSampler.sample line 17
3. lemma OAI.Problem336.PicardSampler.sample_apply_unshifted line 21
4. lemma OAI.Problem336.PicardSampler.measurable_decodedIntegers line 33
5. lemma OAI.Problem336.PicardSampler.measurable_sample line 46
6. theorem OAI.Problem336.PicardSampler.hasLaw_of_slope_coupling line 53
7. theorem OAI.Problem336.PicardSampler.hasLaw_of_integral_coupling line 93
8. def OAI.Problem336.PicardSampler.observation line 124
9. theorem OAI.Problem336.PicardSampler.hasLaw_of_brownian_innovation line 128