OAI/Probability/SLE/BrownianGenerators.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Brownian Generators for chordal SLE.

  1. structure OAI.SLEExactGauge.SmoothTimeBrownianField line 15
  2. def OAI.SLEExactGauge.brownianFieldDrift line 34
  3. lemma OAI.SLEExactGauge.brownian_increment_indep_natural line 39
  4. lemma OAI.SLEExactGauge.brownian_increment_indep_adapted line 49
  5. lemma OAI.SLEExactGauge.gaussian_square_memLp_two line 58
  6. lemma OAI.SLEExactGauge.gaussian_centered_square_memLp_two line 68
  7. lemma OAI.SLEExactGauge.gaussian_square_integral line 74
  8. lemma OAI.SLEExactGauge.gaussian_centered_square_integral line 80
  9. lemma OAI.SLEExactGauge.real_second_taylor_bound line 91
  10. def OAI.SLEExactGauge.standardGaussianAbsMoment line 121
  11. lemma OAI.SLEExactGauge.standardGaussianAbsMoment_nonneg line 124
  12. lemma OAI.SLEExactGauge.gaussian_abs_moment_integrable line 127
  13. lemma OAI.SLEExactGauge.gaussian_abs_moment line 134
  14. lemma OAI.SLEExactGauge.gaussian_abs_cube line 151
  15. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.eval_measurable line 158
  16. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.eval_adapted line 166
  17. lemma OAI.SLEExactGauge.brownian_increment_orthogonal line 175
  18. lemma OAI.SLEExactGauge.brownian_centered_square_orthogonal line 189
  19. lemma OAI.SLEExactGauge.brownian_set_integral_increment_zero line 205
  20. lemma OAI.SLEExactGauge.brownian_set_integral_square line 221
  21. lemma OAI.SLEExactGauge.smooth_field_taylor_set_error line 252
  22. lemma OAI.SLEExactGauge.brownian_expected_abs_increment_le line 320
  23. lemma OAI.SLEExactGauge.bounded_interval_integral_integrable line 339
  24. lemma OAI.SLEExactGauge.bounded_interval_integral_expectation_bound line 350
  25. lemma OAI.SLEExactGauge.bounded_time_section_intervalIntegrable line 368
  26. lemma OAI.SLEExactGauge.smooth_field_time_set_error line 377
  27. lemma OAI.SLEExactGauge.smooth_field_second_mean_error line 444
  28. lemma OAI.SLEExactGauge.smooth_field_second_set_error line 508
  29. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.eval_integrable line 566
  30. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.deriv_real_joint line 577
  31. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.drift_real_joint line 587
  32. lemma OAI.SLEExactGauge.bounded_interval_integral_expectation_add line 597
  33. def OAI.SLEExactGauge.dynkinRate line 616
  34. lemma OAI.SLEExactGauge.dynkinRate_tendsto_zero line 620
  35. lemma OAI.SLEExactGauge.abs_dynkin_algebra_bound line 624
  36. lemma OAI.SLEExactGauge.smooth_field_one_step_error line 638