OAI/Probability/FreeIsing/Brownian/IntegralProperties.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.BrownianGrid.uniformSum_stronglyMeasurable_terminal line 13
2. theorem OAI.Problem367.BrownianGrid.integral_integralSum_eq_zero line 38
3. theorem OAI.Problem367.BrownianGrid.integral_sq_error_tendsto_of_Lp_tendsto line 60
4. theorem OAI.Problem367.BrownianGrid.uniformSumLp_limit_terminal_centered line 81
5. theorem OAI.Problem367.BrownianGrid.exists_terminal_uniform_integral line 112
6. theorem OAI.Problem367.BrownianGrid.ae_eq_of_mean_square_limits line 136
7. theorem OAI.Problem367.BrownianGrid.exists_terminal_uniform_integral_of_bounded_continuous line 155