OAI/Probability/FreeIsing/Stochastic/StoppedBrownianCross.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.StoppedBrownianCross.product_martingale_of_increment_product_zero line 15
2. theorem OAI.Problem367.StoppedBrownianCross.increment_product_condExp_zero line 61
3. theorem OAI.Problem367.StoppedBrownianCross.brownian_product_martingale line 96
4. theorem OAI.Problem367.StoppedBrownianCross.intervalSum_memLp_two_of_bounded line 129
5. theorem OAI.Problem367.StoppedBrownianCross.intervalSum_product_martingale line 138
6. theorem OAI.Problem367.StoppedBrownianCross.stopped_predictable_sum_product_martingale line 179
7. theorem OAI.Problem367.StoppedBrownianCross.stopped_brownian_sum_product_martingale line 271
8. theorem OAI.Problem367.StoppedBrownianCross.integral_stopped_sum_product_eq_zero line 311