OAI/Probability/SLE/IntervalDensity.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Interval Density for chordal SLE.

  1. def OAI.SLEExactGauge.smoothingWidth line 15
  2. lemma OAI.SLEExactGauge.smoothingWidth_pos line 17
  3. lemma OAI.SLEExactGauge.smoothingWidth_le line 21
  4. lemma OAI.SLEExactGauge.smoothingWidth_tendsto line 26
  5. def OAI.SLEExactGauge.intervalBump line 31
  6. lemma OAI.SLEExactGauge.intervalBump_radii line 41
  7. def OAI.SLEExactGauge.intervalDensity line 50
  8. lemma OAI.SLEExactGauge.intervalDensity_smooth line 53
  9. lemma OAI.SLEExactGauge.intervalDensity_nonneg line 57
  10. lemma OAI.SLEExactGauge.intervalDensity_compact line 61
  11. lemma OAI.SLEExactGauge.intervalDensity_integrable line 65
  12. lemma OAI.SLEExactGauge.intervalDensity_integral line 69
  13. lemma OAI.SLEExactGauge.intervalDensity_support line 73
  14. lemma OAI.SLEExactGauge.intervalDensity_bound line 81
  15. lemma OAI.SLEExactGauge.intervalBump_integral_tendsto line 91
  16. lemma OAI.SLEExactGauge.intervalDensity_support_exact line 119
  17. lemma OAI.SLEExactGauge.intervalDensity_tendsto line 126
  18. def OAI.SLEExactGauge.densityPrimitive line 151
  19. lemma OAI.SLEExactGauge.densityPrimitive_hasDerivAt line 154
  20. lemma OAI.SLEExactGauge.densityPrimitive_contDiff line 160
  21. lemma OAI.SLEExactGauge.densityPrimitive_support line 169
  22. lemma OAI.SLEExactGauge.densityPrimitive_compact line 191
  23. lemma OAI.SLEExactGauge.densityPrimitive_bound line 197
  24. def OAI.SLEExactGauge.intervalTransport line 206
  25. lemma OAI.SLEExactGauge.intervalTransport_contDiff line 210
  26. lemma OAI.SLEExactGauge.intervalTransport_hasDerivAt line 214
  27. lemma OAI.SLEExactGauge.intervalTransport_support line 220
  28. lemma OAI.SLEExactGauge.intervalTransport_compact line 241
  29. lemma OAI.SLEExactGauge.intervalTransport_support_interior line 247
  30. lemma OAI.SLEExactGauge.intervalTransport_bound line 255
  31. lemma OAI.SLEExactGauge.intervalTransport_integrable line 274
  32. lemma OAI.SLEExactGauge.intervalTransport_integral_abs_le line 280
  33. def OAI.SLEExactGauge.complexTensor line 303
  34. lemma OAI.SLEExactGauge.complexTensor_contDiff line 305
  35. lemma OAI.SLEExactGauge.complexTensor_support line 310
  36. lemma OAI.SLEExactGauge.complexTensor_compact line 321
  37. lemma OAI.SLEExactGauge.complexTensor_integral line 327
  38. lemma OAI.SLEExactGauge.complexTensor_integral_abs line 337
  39. lemma OAI.SLEExactGauge.complexTensor_deriv_re line 342
  40. lemma OAI.SLEExactGauge.complexTensor_deriv_im line 351
  41. def OAI.SLEExactGauge.rectangleDensity line 360
  42. def OAI.SLEExactGauge.rectangleTransportX line 364
  43. def OAI.SLEExactGauge.rectangleTransportY line 369
  44. lemma OAI.SLEExactGauge.rectangleTransportX_contDiff line 374
  45. lemma OAI.SLEExactGauge.rectangleTransportY_contDiff line 379
  46. lemma OAI.SLEExactGauge.rectangleTransportX_compact line 384
  47. lemma OAI.SLEExactGauge.rectangleTransportY_compact line 390
  48. lemma OAI.SLEExactGauge.rectangleTransportX_support line 396
  49. lemma OAI.SLEExactGauge.rectangleTransportY_support line 407
  50. lemma OAI.SLEExactGauge.rectangleTransport_divergence line 417
  51. lemma OAI.SLEExactGauge.rectangleTransportX_bound line 432
  52. lemma OAI.SLEExactGauge.rectangleTransportY_bound line 442
  53. lemma OAI.SLEExactGauge.intervalDensity_integral_abs line 452
  54. lemma OAI.SLEExactGauge.rectangleTransportX_integral_abs line 457
  55. lemma OAI.SLEExactGauge.rectangleTransportY_integral_abs line 463
  56. def OAI.SLEExactGauge.scaleLength line 469
  57. def OAI.SLEExactGauge.scaleOrigin line 470
  58. lemma OAI.SLEExactGauge.scaleLength_pos line 472
  59. lemma OAI.SLEExactGauge.scaleLength_le_one line 474
  60. lemma OAI.SLEExactGauge.scaleLength_zero line 477
  61. lemma OAI.SLEExactGauge.scaleLength_succ line 478
  62. lemma OAI.SLEExactGauge.scaleOrigin_zero line 480
  63. lemma OAI.SLEExactGauge.scaleOrigin_nonneg line 481
  64. lemma OAI.SLEExactGauge.scaleOrigin_add_le_one line 483
  65. lemma OAI.SLEExactGauge.scaleOrigin_step line 488
  66. lemma OAI.SLEExactGauge.scaleOrigin_right_step line 493
  67. lemma OAI.SLEExactGauge.dyadic_position_param line 499
  68. lemma OAI.SLEExactGauge.dyadic_sum line 512
  69. lemma OAI.SLEExactGauge.dyadic_sum_square line 519
  70. theorem OAI.SLEExactGauge.integral_sum_kernel_sq_le line 545
  71. def OAI.SLEExactGauge.openUnitStrip line 588
  72. def OAI.SLEExactGauge.SourceIsStripWeakGradient line 592
  73. def OAI.SLEExactGauge.stripDirichletEnergy line 601
  74. lemma OAI.SLEExactGauge.openUnitStrip_isOpen line 604
  75. lemma OAI.SLEExactGauge.openUnitStrip_measure_lt_top line 610
  76. instance OAI.SLEExactGauge.finite_openUnitStrip line 620