OAI/Probability/SLE/StoppedKernels.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Stopped Kernels for chordal SLE.

  1. lemma OAI.SLEExactGauge.diskLogRadius_laplacian line 15
  2. lemma OAI.SLEExactGauge.diskLogRadius_exp line 27
  3. lemma OAI.SLEExactGauge.log_diskWeight_direction_bound line 33
  4. lemma OAI.SLEExactGauge.disk_preSchwarzian_weight line 48
  5. lemma OAI.SLEExactGauge.diskLogRadius_direction_bound line 65
  6. lemma OAI.SLEExactGauge.diskLogRadius_gradient_bound line 91
  7. def OAI.SLEExactGauge.layerProfile line 121
  8. def OAI.SLEExactGauge.layerProfileDeriv line 124
  9. lemma OAI.SLEExactGauge.layerProfile_hasDeriv line 128
  10. lemma OAI.SLEExactGauge.layerProfileDeriv_hasDeriv line 139
  11. lemma OAI.SLEExactGauge.layerProfile_contDiff line 154
  12. lemma OAI.SLEExactGauge.layerProfile_nonneg line 158
  13. lemma OAI.SLEExactGauge.layerProfile_le line 162
  14. lemma OAI.SLEExactGauge.layerProfile_deriv_nonneg line 168
  15. lemma OAI.SLEExactGauge.layerProfile_second_le line 174
  16. lemma OAI.SLEExactGauge.layerProfile_deriv_lower line 187
  17. def OAI.SLEExactGauge.layerExponent line 222
  18. lemma OAI.SLEExactGauge.layerExponent_pos line 224
  19. lemma OAI.SLEExactGauge.layerExponent_le_one line 225
  20. lemma OAI.SLEExactGauge.layerExponent_gradient line 229
  21. def OAI.SLEExactGauge.diskLayerBarrier line 236
  22. lemma OAI.SLEExactGauge.diskLayerBarrier_bounds line 239
  23. lemma OAI.SLEExactGauge.diskLayerBarrier_contDiffAt line 243
  24. lemma OAI.SLEExactGauge.diskLayerBarrier_laplacian_le line 249
  25. lemma OAI.SLEExactGauge.diskLayerBarrier_superharmonic line 283
  26. lemma OAI.SLEExactGauge.diskLayerBarrier_layer_lower line 294
  27. lemma OAI.SLEExactGauge.conformal_layer_measurable line 326
  28. lemma OAI.SLEExactGauge.disk_conformal_layer_green_le line 336
  29. lemma OAI.SLEExactGauge.complex_derivative_det line 390
  30. lemma OAI.SLEExactGauge.conformal_disk_area_change line 395
  31. lemma OAI.SLEExactGauge.chart_deriv_ne_zero line 407
  32. lemma OAI.SLEExactGauge.disk_radius_le_frontier_distance line 435
  33. def OAI.SLEExactGauge.layerGreenConstant line 471
  34. lemma OAI.SLEExactGauge.layerGreenConstant_pos line 474
  35. lemma OAI.SLEExactGauge.centered_boundary_layer_green_le line 478
  36. def OAI.SLEExactGauge.halfPlaneToDisk line 544
  37. lemma OAI.SLEExactGauge.halfPlane_denominator_ne line 546
  38. lemma OAI.SLEExactGauge.halfPlaneToDisk_maps line 553
  39. lemma OAI.SLEExactGauge.halfPlaneToDisk_differentiable line 558
  40. lemma OAI.SLEExactGauge.halfPlaneToDisk_diskToHalfPlane line 563
  41. lemma OAI.SLEExactGauge.diskToHalfPlane_deriv line 574
  42. lemma OAI.SLEExactGauge.diskToHalfPlane_second_zero line 580
  43. def OAI.SLEExactGauge.halfPlaneGreen line 606
  44. lemma OAI.SLEExactGauge.hasDerivWithinAt_log_norm line 609
  45. lemma OAI.SLEExactGauge.hasDerivWithinAt_conj line 623
  46. lemma OAI.SLEExactGauge.hasDerivWithinAt_log_norm_div line 628
  47. lemma OAI.SLEExactGauge.green_decrease_algebra line 638