OAI/Probability/SpanningForest/BrownianReference.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.BrownianReference.coupling line 15
2. instance OAI.Problem336.BrownianReference.coupling_probability line 17
3. theorem OAI.Problem336.BrownianReference.hidden_hasLaw line 22
4. theorem OAI.Problem336.BrownianReference.noise_coordinate_preserving line 25
5. theorem OAI.Problem336.BrownianReference.independent_samples line 29
6. theorem OAI.Problem336.BrownianReference.independent_processes line 37
7. theorem OAI.Problem336.BrownianReference.hidden_independent_field line 42
8. theorem OAI.Problem336.BrownianReference.measurable_process line 50
9. theorem OAI.Problem336.BrownianReference.preBrownian_process line 54
10. theorem OAI.Problem336.BrownianReference.brownian_process line 60
11. theorem OAI.Problem336.BrownianReference.bridge_independent_hidden_endpoint line 65