OAI/Probability/SLE/DyadicStrips.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Dyadic Strips for chordal SLE.

  1. lemma OAI.SLEExactGauge.inv_pow_rpow_two line 18
  2. theorem OAI.SLEExactGauge.sle_dyadic_strip_rectangle_hit line 28
  3. theorem OAI.SLEExactGauge.ordinary_sle_strip_hitting_constants line 49
  4. def OAI.SLEExactGauge.IsStripWeakGradient line 72
  5. def OAI.SLEExactGauge.annulusKernel line 81
  6. lemma OAI.SLEExactGauge.measurable_annulusKernel line 84
  7. lemma OAI.SLEExactGauge.lintegral_inv_Ioo line 91
  8. lemma OAI.SLEExactGauge.annulusKernel_polar line 108
  9. theorem OAI.SLEExactGauge.annulusKernel_integral line 121
  10. lemma OAI.SLEExactGauge.complex_deriv_real_det line 151
  11. theorem OAI.SLEExactGauge.univalent_annulus_dirichlet_bound line 158
  12. def OAI.SLEExactGauge.truncatedConformalLog line 178
  13. lemma OAI.SLEExactGauge.lipschitz_clip line 181
  14. lemma OAI.SLEExactGauge.norm_fderiv_clip_le line 186
  15. lemma OAI.SLEExactGauge.norm_fderiv_log_norm_div_le line 197
  16. lemma OAI.SLEExactGauge.truncatedConformalLog_eq_zero line 223
  17. lemma OAI.SLEExactGauge.truncatedConformalLog_eq_height line 230
  18. lemma OAI.SLEExactGauge.fderiv_truncated_eq_zero_of_low line 238
  19. lemma OAI.SLEExactGauge.fderiv_truncated_eq_zero_of_high line 246
  20. lemma OAI.SLEExactGauge.norm_fderiv_truncated_le line 254
  21. lemma OAI.SLEExactGauge.truncated_log_energy_pointwise line 267
  22. lemma OAI.SLEExactGauge.truncated_log_lipschitz_near line 290
  23. theorem OAI.SLEExactGauge.truncated_log_ae_differentiable line 318
  24. lemma OAI.SLEExactGauge.local_lipschitz_weak_derivative line 334
  25. theorem OAI.SLEExactGauge.truncated_log_weak_derivative line 386
  26. lemma OAI.SLEExactGauge.open_univalent_weighted_area line 395
  27. theorem OAI.SLEExactGauge.truncated_log_dirichlet_bound line 415
  28. lemma OAI.SLEExactGauge.measurable_real_gradient line 453
  29. lemma OAI.SLEExactGauge.norm_real_gradient line 456
  30. theorem OAI.SLEExactGauge.truncated_log_sobolev_energy line 459
  31. def OAI.SLEExactGauge.conformalStripLog line 488
  32. lemma OAI.SLEExactGauge.exp_strip_halfplane line 491
  33. lemma OAI.SLEExactGauge.exp_injective_strip line 498
  34. theorem OAI.SLEExactGauge.conformal_strip_total_energy line 505
  35. lemma OAI.SLEExactGauge.truncated_log_continuousOn line 531
  36. lemma OAI.SLEExactGauge.truncated_log_bounds line 539
  37. theorem OAI.SLEExactGauge.conformal_unit_strip_weak_gradient line 543
  38. def OAI.SLEExactGauge.sphericalTruncatedLog line 567
  39. lemma OAI.SLEExactGauge.sphericalTruncatedLog_coe line 570
  40. lemma OAI.SLEExactGauge.sphericalTruncatedLog_infty line 574
  41. lemma OAI.SLEExactGauge.sphericalTruncatedLog_continuous line 577
  42. theorem OAI.SLEExactGauge.spherical_strip_log_continuous line 604
  43. theorem OAI.SLEExactGauge.source_strip_log_regularity line 620