OAI/Probability/FreeIsing/Conditioning/CopyFiltration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.ConditionalCopyBrownian.pastPath_comap_mono line 14
2. theorem OAI.Problem367.ConditionalCopyBrownian.joinedPast_eq_sup line 26
3. theorem OAI.Problem367.ConditionalCopyBrownian.joinedPast_mono line 39
4. def OAI.Problem367.ConditionalCopyBrownian.joinedFiltration line 56
5. theorem OAI.Problem367.ConditionalCopyBrownian.joinedFiltration_apply line 64
6. theorem OAI.Problem367.ConditionalCopyArrayBrownian.commonNoise_martingale_joinedFiltration line 77
7. theorem OAI.Problem367.ConditionalCopyArrayBrownian.isBrownian_commonNoise line 91