OAI/Probability/FreeIsing/Brownian/IntegralHorizon.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.BrownianIntegralProcess.uniformGrid_nat_horizon line 15
2. theorem OAI.Problem367.BrownianIntegralProcess.stoppedUniformSum_nat_horizon_le line 28
3. theorem OAI.Problem367.BrownianIntegralProcess.stoppedUniformSum_nat_horizon line 54
4. theorem OAI.Problem367.BrownianIntegralProcess.ae_eq_of_nat_horizon_meanSquare_limits line 62
5. theorem OAI.Problem367.BrownianIntegralProcess.exists_global_of_compatible_integer_martingales line 88
6. theorem OAI.Problem367.BrownianIntegralProcess.exists_global_continuous_uniform_integral line 125