OAI/Probability/FreeIsing/Stochastic/ContinuousCopyBrownian.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.Problem367.ContinuousCopyBrownian.Jointline 16 - def
OAI.Problem367.ContinuousCopyBrownian.historyline 18 - theorem
OAI.Problem367.ContinuousCopyBrownian.measurable_historyline 21 - theorem
OAI.Problem367.ContinuousCopyBrownian.history_historyline 26 - abbrev
OAI.Problem367.ContinuousCopyBrownian.pastSpaceline 30 - def
OAI.Problem367.ContinuousCopyBrownian.joinedFiltrationline 33 - theorem
OAI.Problem367.ContinuousCopyBrownian.isBrownian_commonNoiseline 41 - theorem
OAI.Problem367.ContinuousCopyBrownian.condExp_increment_eq_zeroline 51 - theorem
OAI.Problem367.ContinuousCopyBrownian.commonNoise_martingaleline 82