OAI/Probability/FreeIsing/Spectral/L2CompensatedSquareStopping.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.L2CompensatedSquareStopping.exists_integrable_horizon_envelope line 22
2. theorem OAI.Problem367.L2CompensatedSquareStopping.martingale_rightCont line 33
3. theorem OAI.Problem367.L2CompensatedSquareStopping.martingale_stoppedProcess_rightCont line 37
4. theorem OAI.Problem367.L2CompensatedSquareStopping.exists_integrable_compensatedSquare_envelope line 51
5. theorem OAI.Problem367.L2CompensatedSquareStopping.compensatedSquare_martingale_rightCont line 70
6. theorem OAI.Problem367.L2CompensatedSquareStopping.stopped_compensatedSquare_rightCont line 78