OAI/Probability/SLE/SausagePointBound.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Sausage Point Bound for chordal SLE.

  1. def OAI.SLEExactGauge.spatialSmallnessConstant line 16
  2. def OAI.SLEExactGauge.spatialOnePointConstant line 17
  3. lemma OAI.SLEExactGauge.spatialSmallnessConstant_gt_one line 20
  4. lemma OAI.SLEExactGauge.spatial_smallness line 25
  5. lemma OAI.SLEExactGauge.initialGreen_le_height line 39
  6. def OAI.SLEExactGauge.sausagePointConstant line 51
  7. lemma OAI.SLEExactGauge.spatialOnePointConstant_pos line 55
  8. lemma OAI.SLEExactGauge.sausagePointConstant_pos line 60
  9. lemma OAI.SLEExactGauge.negative_power_scale line 65
  10. theorem OAI.SLEExactGauge.normalized_visit_bound line 76
  11. lemma OAI.SLEExactGauge.IsOrdinaryChordalSLE.exists_charts line 150
  12. lemma OAI.SLEExactGauge.sle_high_center_approach line 170
  13. def OAI.SLEExactGauge.boundaryApproachPower line 208
  14. def OAI.SLEExactGauge.annularApproachPower line 209
  15. def OAI.SLEExactGauge.annularApproachConstant line 211
  16. lemma OAI.SLEExactGauge.annularApproachPower_pos line 214
  17. lemma OAI.SLEExactGauge.annularApproachConstant_pos line 220
  18. lemma OAI.SLEExactGauge.sle_low_center_approach line 228
  19. theorem OAI.SLEExactGauge.sle_annular_small_target line 283
  20. lemma OAI.SLEExactGauge.sle_high_center_approach_scaled line 322
  21. lemma OAI.SLEExactGauge.sle_low_center_approach_scaled line 366
  22. theorem OAI.SLEExactGauge.sle_annular_small_target_scaled line 421
  23. lemma OAI.SLEExactGauge.stripRectangle_norm_sub_le line 460
  24. lemma OAI.SLEExactGauge.stripRectangle_exp_distance line 474
  25. def OAI.SLEExactGauge.stripHittingConstant line 506
  26. lemma OAI.SLEExactGauge.stripHittingConstant_pos line 509
  27. theorem OAI.SLEExactGauge.sle_exp_strip_rectangle_hit line 518