OAI/Probability/FreeIsing/Martingales/RandomEvaluation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.MartingaleRandomEvaluation.stronglyMeasurable_random_evaluation line 14
2. theorem OAI.Problem367.MartingaleRandomEvaluation.aestronglyMeasurable_random_evaluation line 25
3. theorem OAI.Problem367.MartingaleRandomEvaluation.integrable_sq_random_evaluation line 37
4. theorem OAI.Problem367.MartingaleRandomEvaluation.memLp_random_evaluation line 50
5. theorem OAI.Problem367.MartingaleRandomEvaluation.integral_sq_random_evaluation_le line 60
6. theorem OAI.Problem367.MartingaleRandomEvaluation.tendsto_integral_sq_random_evaluation_sub line 73