OAI/Probability/SLE/IntegralLimits.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Integral Limits for chordal SLE.

  1. lemma OAI.SLEExactGauge.BrownianPredictable.predictableTerm_square_integral line 41
  2. theorem OAI.SLEExactGauge.BrownianPredictable.predictableFeatureSum_second_moment line 54
  3. lemma OAI.SLEExactGauge.BrownianPredictable.centeredSquare_gaussian_memLp line 92
  4. lemma OAI.SLEExactGauge.BrownianPredictable.centeredSquare_gaussian_mean line 96
  5. lemma OAI.SLEExactGauge.BrownianPredictable.centeredSquare_gaussian_second_moment line 102
  6. theorem OAI.SLEExactGauge.BrownianPredictable.brownian_predictableSum_isometry line 109
  7. theorem OAI.SLEExactGauge.BrownianPredictable.brownian_predictableQuadraticError_isometry line 126
  8. def OAI.SLEExactGauge.BrownianPredictable.dyadicTime line 145
  9. lemma OAI.SLEExactGauge.BrownianPredictable.dyadicTime_mono line 148
  10. lemma OAI.SLEExactGauge.BrownianPredictable.dyadicTime_step line 152
  11. def OAI.SLEExactGauge.BrownianPredictable.dyadicQuadraticError line 160
  12. lemma OAI.SLEExactGauge.BrownianPredictable.dyadicQuadraticError_memLp line 166
  13. lemma OAI.SLEExactGauge.BrownianPredictable.dyadicQuadraticError_integral line 181
  14. lemma OAI.SLEExactGauge.BrownianPredictable.dyadicQuadraticError_second_moment_le line 205
  15. theorem OAI.SLEExactGauge.BrownianPredictable.brownian_dyadic_weighted_quadraticError_tendsto line 238
  16. lemma OAI.SLEExactGauge.L2Limit.eLpNorm_two_eq_integral_sq line 288
  17. lemma OAI.SLEExactGauge.L2Limit.uniformIntegrable_one_of_eLpNorm_two_bounded line 300
  18. theorem OAI.SLEExactGauge.L2Limit.integral_tendsto_of_ae_of_square_bound line 345
  19. def OAI.SLEExactGauge.PredictableLimit.dyadicDriverSum line 370
  20. lemma OAI.SLEExactGauge.PredictableLimit.dyadicDriverSum_memLp line 375
  21. lemma OAI.SLEExactGauge.PredictableLimit.dyadicDriverSum_integral line 388
  22. lemma OAI.SLEExactGauge.PredictableLimit.dyadicDriverSum_second_moment_le line 406
  23. theorem OAI.SLEExactGauge.PredictableLimit.limit_centered line 437
  24. def OAI.SLEExactGauge.TaylorMeshes.remainder₂ line 463
  25. lemma OAI.SLEExactGauge.TaylorMeshes.quadratic_taylor_bound line 466
  26. lemma OAI.SLEExactGauge.TaylorMeshes.sum_remainder₂_bound line 497
  27. def OAI.SLEExactGauge.TaylorMeshes.mesh line 521
  28. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_zero line 523
  29. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_end line 524
  30. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_step line 527
  31. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_mono line 530
  32. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_mem line 533
  33. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_step_tendsto line 538
  34. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_increments_small line 546
  35. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_taylor_remainder_tendsto line 561
  36. lemma OAI.SLEExactGauge.TaylorMeshes.mesh_riemann_tendsto line 595
  37. lemma OAI.SLEExactGauge.TimeField.sum_family_remainder₂_bound line 661