OAI/Probability/SLE/OptionalStopping.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Optional Stopping for chordal SLE.

  1. lemma OAI.SLEExactGauge.eq_of_uniform_small_increment line 13
  2. lemma OAI.SLEExactGauge.bounded_interval_integral_expectation_sub line 62
  3. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.generator_measurable line 79
  4. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.generator_bound line 90
  5. theorem OAI.SLEExactGauge.brownian_time_field_dynkin line 106
  6. def OAI.SLEExactGauge.stopGridIndex line 160
  7. def OAI.SLEExactGauge.stopGridTime line 163
  8. def OAI.SLEExactGauge.stopGrid line 166
  9. lemma OAI.SLEExactGauge.stopGridIndex_le line 169
  10. lemma OAI.SLEExactGauge.stopGrid_bounds line 174
  11. lemma OAI.SLEExactGauge.stopGrid_tendsto line 188
  12. lemma OAI.SLEExactGauge.measurable_discrete_eval line 196
  13. lemma OAI.SLEExactGauge.stopping_time_measurable_nnreal line 201
  14. lemma OAI.SLEExactGauge.stopGridIndex_measurable line 206
  15. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.time_increment_all line 211
  16. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.time_dist_le line 221
  17. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.space_lipschitz line 233
  18. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.path_continuous line 243
  19. lemma OAI.SLEExactGauge.cumulative_integral_measurable line 264
  20. def OAI.SLEExactGauge.brownianFieldCompensated line 280
  21. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.compensated_integrable line 284
  22. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.compensated_past_integral_zero line 296
  23. lemma OAI.SLEExactGauge.sum_stopped_increments line 320
  24. lemma OAI.SLEExactGauge.finite_grid_stopped_integral_eq line 337
  25. lemma OAI.SLEExactGauge.monotone_stopGridTime line 368
  26. def OAI.SLEExactGauge.gridFiltration line 373
  27. lemma OAI.SLEExactGauge.brownian_compensated_grid_integral line 379
  28. lemma OAI.SLEExactGauge.bounded_cumulative_at_grid line 415
  29. theorem OAI.SLEExactGauge.brownian_time_field_optional line 443
  30. def OAI.SLEExactGauge.picardApprox line 503
  31. lemma OAI.SLEExactGauge.picardApprox_measurable line 509
  32. lemma OAI.SLEExactGauge.picardApprox_eq_iterate line 532
  33. theorem OAI.SLEExactGauge.exists_measurable_bounded_ode line 555
  34. def OAI.SLEExactGauge.clippedHeight line 618
  35. def OAI.SLEExactGauge.clippedCenter line 621
  36. def OAI.SLEExactGauge.clippedLogLoewnerField line 624
  37. lemma OAI.SLEExactGauge.clippedHeight_pos line 630
  38. lemma OAI.SLEExactGauge.clippedHeight_bounds line 633
  39. lemma OAI.SLEExactGauge.clippedCenter_im line 638
  40. lemma OAI.SLEExactGauge.clippedCenter_ne_zero line 642
  41. lemma OAI.SLEExactGauge.exp_clamp_lipschitz line 649