OAI/Probability/FreeIsing/Brownian/UniformSumCongruence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.BrownianGrid.integralSum_congr_ae line 12
2. theorem OAI.Problem367.BrownianGrid.uniformSum_congr_ae line 21
3. theorem OAI.Problem367.BrownianGrid.integral_uniformSum_sq_error_congr_ae line 30
4. theorem OAI.Problem367.BrownianGrid.uniform_meanSquare_limit_congr_ae line 41
5. theorem OAI.Problem367.BrownianGrid.uniformSum_comp_congr_ae line 53
6. theorem OAI.Problem367.BrownianGrid.uniform_meanSquare_limit_comp_congr_ae line 62