OAI/Probability/FreeIsing/Conditioning/CopyBrownian.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.ConditionalCopyBrownian.joinedHistory line 16
2. theorem OAI.Problem367.ConditionalCopyBrownian.measurable_joinedHistory line 20
3. abbrev OAI.Problem367.ConditionalCopyBrownian.joinedPast line 26
4. theorem OAI.Problem367.ConditionalCopyBrownian.joinedPast_le line 30
5. theorem OAI.Problem367.ConditionalCopyBrownian.condExp_future_eq_integral line 36
6. theorem OAI.Problem367.ConditionalCopyBrownian.condExp_increment_eq_zero line 67
7. theorem OAI.Problem367.ConditionalCopyBrownian.condExp_increment_sq_eq_elapsed line 90
8. theorem OAI.Problem367.ConditionalCopyBrownian.isPreBrownian_commonNoise line 115
9. theorem OAI.Problem367.ConditionalCopyBrownian.commonNoise_martingale line 125