OAI/Probability/FreeIsing/Conditioning/ContinuousCopyImmersion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.ContinuousCopyBrownian.singleHistory line 16
2. lemma OAI.Problem367.ContinuousCopyBrownian.measurable_singleHistory line 19
3. lemma OAI.Problem367.ContinuousCopyBrownian.singleHistory_singleHistory line 23
4. def OAI.Problem367.ContinuousCopyBrownian.singleFiltration line 27
5. lemma OAI.Problem367.ContinuousCopyBrownian.measurable_noisePast_singleFiltration line 38
6. lemma OAI.Problem367.ContinuousCopyBrownian.joinedFiltration_eq_left line 43
7. theorem OAI.Problem367.ContinuousCopyBrownian.exists_past_kernel line 69
8. theorem OAI.Problem367.ContinuousCopyBrownian.martingale_left_of_future_indep line 82
9. lemma OAI.Problem367.ContinuousCopyBrownian.measurable_swap_joinedFiltration line 97
10. theorem OAI.Problem367.ContinuousCopyBrownian.martingale_right_of_future_indep line 111