OAI/Probability/SLE/LoewnerReflection.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Loewner Reflection for chordal SLE.

  1. def OAI.SLEExactGauge.loewnerMirror line 17
  2. lemma OAI.SLEExactGauge.loewnerMirror_apply line 25
  3. lemma OAI.SLEExactGauge.loewnerMirror_twice line 26
  4. lemma OAI.SLEExactGauge.loewnerMirror_im line 27
  5. lemma OAI.SLEExactGauge.loewnerMirror_re line 28
  6. lemma OAI.SLEExactGauge.loewnerMirror_dist line 29
  7. lemma OAI.SLEExactGauge.loewnerMirror_norm line 31
  8. lemma OAI.SLEExactGauge.loewnerMirror_bounded line 33
  9. lemma OAI.SLEExactGauge.loewnerMirror_free line 38
  10. lemma OAI.SLEExactGauge.loewnerMirror_free_image line 51
  11. lemma OAI.SLEExactGauge.loewnerMirror_surviving line 63
  12. lemma OAI.SLEExactGauge.mirror_conjugate_differentiable line 85
  13. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.mirror line 100
  14. def OAI.SLEExactGauge.rightCenter line 174
  15. def OAI.SLEExactGauge.rightField line 177
  16. lemma OAI.SLEExactGauge.rightCenter_re line 179
  17. lemma OAI.SLEExactGauge.rightCenter_norm line 182
  18. lemma OAI.SLEExactGauge.rightCenter_ne_zero line 185
  19. lemma OAI.SLEExactGauge.rightCenter_eq line 188
  20. lemma OAI.SLEExactGauge.rightCenter_dist line 191
  21. lemma OAI.SLEExactGauge.rightField_bound line 209
  22. lemma OAI.SLEExactGauge.rightField_lipschitz line 216
  23. lemma OAI.SLEExactGauge.continuous_rightField line 232
  24. lemma OAI.SLEExactGauge.rightField_eq line 241
  25. def OAI.SLEExactGauge.reverseCenter line 255
  26. def OAI.SLEExactGauge.reverseField line 258
  27. lemma OAI.SLEExactGauge.reverseCenter_im line 260
  28. lemma OAI.SLEExactGauge.reverseCenter_norm line 263
  29. lemma OAI.SLEExactGauge.reverseCenter_ne_zero line 266
  30. lemma OAI.SLEExactGauge.reverseCenter_eq line 269
  31. lemma OAI.SLEExactGauge.reverseCenter_dist line 272
  32. lemma OAI.SLEExactGauge.reverseField_bound line 290
  33. lemma OAI.SLEExactGauge.reverseField_lipschitz line 297
  34. lemma OAI.SLEExactGauge.continuous_reverseField line 313
  35. lemma OAI.SLEExactGauge.exists_random_initial_bounded_flow line 333
  36. lemma OAI.SLEExactGauge.exists_measurable_reverse_flow line 359
  37. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.reverse_path_derivative line 386
  38. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.reverse_flow_identifies line 408
  39. lemma OAI.SLEExactGauge.exists_measurable_right_flow line 437
  40. def OAI.SLEExactGauge.positiveBoundaryField line 474
  41. lemma OAI.SLEExactGauge.positiveBoundaryField_eq line 477
  42. lemma OAI.SLEExactGauge.positiveBoundaryField_bound line 481
  43. lemma OAI.SLEExactGauge.positiveBoundaryField_lipschitz line 488
  44. lemma OAI.SLEExactGauge.continuous_positiveBoundaryField line 508
  45. theorem OAI.SLEExactGauge.positive_boundary_global_adapted_solution line 527
  46. def OAI.SLEExactGauge.boundaryClockField line 594
  47. lemma OAI.SLEExactGauge.clipped_real_inv_bound line 597
  48. lemma OAI.SLEExactGauge.clipped_real_inv_lipschitz line 602
  49. lemma OAI.SLEExactGauge.boundaryClockField_bound line 616
  50. lemma OAI.SLEExactGauge.boundaryClockField_lipschitz line 627
  51. lemma OAI.SLEExactGauge.continuous_boundaryClockField line 661
  52. theorem OAI.SLEExactGauge.boundary_clock_global_adapted_solution line 685
  53. structure OAI.SLEExactGauge.BoundaryClockSolution line 755
  54. lemma OAI.SLEExactGauge.exists_boundaryClockSolution line 768