OAI/Probability/SLE/AngularLaws.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Angular Laws for chordal SLE.

  1. def OAI.SLEExactGauge.greenInner line 14
  2. def OAI.SLEExactGauge.greenOuter line 15
  3. lemma OAI.SLEExactGauge.greenInner_pos line 17
  4. lemma OAI.SLEExactGauge.greenInner_le_half line 19
  5. lemma OAI.SLEExactGauge.greenInner_le_outer line 26
  6. lemma OAI.SLEExactGauge.greenOuter_pos line 30
  7. lemma OAI.SLEExactGauge.greenOuter_lt_one line 33
  8. lemma OAI.SLEExactGauge.greenInner_tendsto line 37
  9. lemma OAI.SLEExactGauge.greenOuter_tendsto line 42
  10. lemma OAI.SLEExactGauge.greenInner_log_tendsto line 46
  11. def OAI.SLEExactGauge.polarUnitDisk line 50
  12. def OAI.SLEExactGauge.polarGreenTarget line 52
  13. lemma OAI.SLEExactGauge.greenTruncation_tendsto line 56
  14. lemma OAI.SLEExactGauge.polar_green_le line 75
  15. lemma OAI.SLEExactGauge.polarPoint_eq_polarCoord line 120
  16. lemma OAI.SLEExactGauge.disk_log_lintegral_polar line 127
  17. lemma OAI.SLEExactGauge.disk_green_le line 173
  18. lemma OAI.SLEExactGauge.second_direction_chain line 196
  19. lemma OAI.SLEExactGauge.plane_laplacian_chain line 235
  20. def OAI.SLEExactGauge.diskWeight line 255
  21. lemma OAI.SLEExactGauge.diskWeight_pos line 257
  22. lemma OAI.SLEExactGauge.diskWeight_contDiff line 262
  23. lemma OAI.SLEExactGauge.diskWeight_fderiv line 265
  24. lemma OAI.SLEExactGauge.diskWeight_laplacian line 273
  25. lemma OAI.SLEExactGauge.log_diskWeight_laplacian line 284
  26. lemma OAI.SLEExactGauge.log_norm_direction_bound line 313
  27. lemma OAI.SLEExactGauge.univalent_omitted_value_bound_ball line 349
  28. lemma OAI.SLEExactGauge.logarithmic_lift_deriv_bound line 396
  29. lemma OAI.SLEExactGauge.logarithmic_lift_second_bound line 418
  30. lemma OAI.SLEExactGauge.exists_omitted_near_of_inverse line 444
  31. lemma OAI.SLEExactGauge.preSchwarzian_bound_of_inverse line 492
  32. lemma OAI.SLEExactGauge.preSchwarzian_bound_ball line 552
  33. lemma OAI.SLEExactGauge.disk_preSchwarzian_bound line 614
  34. def OAI.SLEExactGauge.diskLogRadius line 653
  35. lemma OAI.SLEExactGauge.diskLogRadius_contDiffAt line 656