OAI/Probability/SLE/ItoIsometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Ito Isometry for chordal SLE.

  1. lemma OAI.SLEExactGauge.TimeField.mesh_family_remainder_tendsto line 48
  2. lemma OAI.SLEExactGauge.TimeField.mesh_time_increment_tendsto line 84
  3. lemma OAI.SLEExactGauge.BrownianIto.coe_dyadicTime line 171
  4. lemma OAI.SLEExactGauge.BrownianIto.mesh_toNNReal line 177
  5. def OAI.SLEExactGauge.BrownianIto.derivativeSum line 183
  6. def OAI.SLEExactGauge.BrownianIto.quadraticSum line 188
  7. lemma OAI.SLEExactGauge.BrownianIto.error_one_eq line 193
  8. lemma OAI.SLEExactGauge.BrownianIto.quadraticSum_tendsto line 202
  9. def OAI.SLEExactGauge.BrownianField.fieldSum line 218
  10. structure OAI.SLEExactGauge.BrownianField.FieldRegular line 225
  11. theorem OAI.SLEExactGauge.BrownianField.fieldSum_tendsto line 235
  12. theorem OAI.SLEExactGauge.BrownianField.field_ito_centered line 311
  13. def OAI.SLEExactGauge.ClippedLogSolution.velocity line 353
  14. lemma OAI.SLEExactGauge.ClippedLogSolution.velocity_continuous line 357
  15. lemma OAI.SLEExactGauge.ClippedLogSolution.compact_field_regular line 368
  16. lemma OAI.SLEExactGauge.natural_eq_pastSigma line 399
  17. lemma OAI.SLEExactGauge.mesh_eq_dyadicTime line 403
  18. lemma OAI.SLEExactGauge.ClippedLogSolution.partial_adapted line 407
  19. theorem OAI.SLEExactGauge.ClippedLogSolution.compact_field_ito line 420
  20. lemma OAI.SLEExactGauge.prefix_const_sum_le line 461
  21. lemma OAI.SLEExactGauge.mesh_prefix_riemann_error line 471
  22. lemma OAI.SLEExactGauge.mesh_prefix_riemann_tendsto line 530
  23. lemma OAI.SLEExactGauge.mesh_prefix_remainder_tendsto line 546
  24. lemma OAI.SLEExactGauge.mesh_prefix_time_increment_tendsto line 586
  25. def OAI.SLEExactGauge.stoppedDyadicIndex line 679
  26. lemma OAI.SLEExactGauge.lt_stoppedDyadicIndex line 682
  27. lemma OAI.SLEExactGauge.stoppedDyadicIndex_le line 687