OAI/Probability/FreeIsing/Martingales/SpatialPredictableL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.PredictableL2.memLp_two_mul_of_indep line 11
2. theorem OAI.Problem367.PredictableL2.weighted_array_orthogonal line 22
3. theorem OAI.Problem367.PredictableL2.independent_weighted_second_moment line 43
4. theorem OAI.Problem367.PredictableL2.exists_independent_weighted_sum line 53