OAI/Probability/SLE/BrownianStrongMarkov.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Brownian Strong Markov for chordal SLE.

  1. def OAI.SLEExactGauge.shiftedFDD line 15
  2. lemma OAI.SLEExactGauge.shiftedFDD_measurable line 24
  3. lemma OAI.SLEExactGauge.shiftedFDD_indep line 30
  4. lemma OAI.SLEExactGauge.shiftedFDD_setIntegral line 40
  5. lemma OAI.SLEExactGauge.shiftedFDD_grid_measurable line 52
  6. lemma OAI.SLEExactGauge.shiftedFDD_grid_setIntegral line 62
  7. lemma OAI.SLEExactGauge.shiftedFDD_grid_tendsto line 83
  8. theorem OAI.SLEExactGauge.brownian_strongMarkov_integral line 95
  9. def OAI.SLEExactGauge.brownianRestart line 125
  10. lemma OAI.SLEExactGauge.brownianRestart_measurable line 134
  11. lemma OAI.SLEExactGauge.brownian_restart_fdd_restrict line 144
  12. theorem OAI.SLEExactGauge.brownian_restart_path_law line 164
  13. lemma OAI.SLEExactGauge.brownian_restart_path_map line 188
  14. lemma OAI.SLEExactGauge.brownian_restart_event_factorizes line 196
  15. theorem OAI.SLEExactGauge.brownian_restart_independent line 213
  16. lemma OAI.SLEExactGauge.measurable_reverse_driver line 247
  17. theorem OAI.SLEExactGauge.inverse_vertical_measurable line 260
  18. theorem OAI.SLEExactGauge.capacity_trace_adapted line 288
  19. def OAI.SLEExactGauge.IsCapacityTwoTrace line 319

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:41 (same declaration text).

  20. def OAI.SLEExactGauge.IsOrdinaryChordalSLE line 324

    Also declared: ComparatorChallenges/SLELowerPositivity.lean:44 (same declaration text).

  21. structure OAI.SLEExactGauge.RegularSLEPresentation line 332
  22. lemma OAI.SLEExactGauge.RegularSLEPresentation.measurePreserving_val line 351
  23. instance OAI.SLEExactGauge.RegularSLEPresentation.probability line 357
  24. def OAI.SLEExactGauge.RegularSLEPresentation.filtration line 362
  25. lemma OAI.SLEExactGauge.RegularSLEPresentation.trace_adapted line 366
  26. lemma OAI.SLEExactGauge.RegularSLEPresentation.trace_continuous line 376
  27. theorem OAI.SLEExactGauge.exists_regular_sle_presentation line 383
  28. theorem OAI.SLEExactGauge.ordinary_positive_real_center_approach line 436
  29. theorem OAI.SLEExactGauge.sle_positive_real_center_approach line 468
  30. lemma OAI.SLEExactGauge.IsOrdinaryChordalSLE.mirror line 498
  31. theorem OAI.SLEExactGauge.sle_real_center_approach line 511
  32. lemma OAI.SLEExactGauge.derivative_close_of_cauchy line 543
  33. lemma OAI.SLEExactGauge.disk_image_of_deriv_close line 585
  34. lemma OAI.SLEExactGauge.bloch_disk line 629
  35. lemma OAI.SLEExactGauge.hasDerivAt_log_lift line 706
  36. lemma OAI.SLEExactGauge.differentiableOn_log_lift line 729
  37. lemma OAI.SLEExactGauge.exists_holomorphic_log_on_ball line 734
  38. lemma OAI.SLEExactGauge.univalent_omitted_value_bound line 759