OAI/Probability/FreeIsing/Ising/CopyBrownian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.IsingCopyBrownian.graph_future_indep line 20
2. theorem OAI.Problem367.IsingCopyBrownian.future_indep_joinedFiltration line 40
3. theorem OAI.Problem367.IsingCopyBrownian.increment_indep_joinedFiltration line 51
4. theorem OAI.Problem367.IsingCopyBrownian.commonNoise_stronglyAdapted line 62
5. theorem OAI.Problem367.IsingCopyBrownian.innovationLaw_coordinate_preBrownian line 70
6. theorem OAI.Problem367.IsingCopyBrownian.commonNoise_isBrownianReal line 79
7. theorem OAI.Problem367.IsingCopyBrownian.commonNoise_martingale line 89
8. theorem OAI.Problem367.IsingCopyBrownian.commonNoise_increments_indep line 100