OAI/Probability/SLELocalization/ConformalKernels.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Layer estimates.

  1. lemma OAI.SLEExactGauge.Layer.logFactor_laplacian line 15
  2. lemma OAI.SLEExactGauge.Layer.logNorm_fderiv line 46
  3. structure OAI.SLEExactGauge.Layer.DiskPair line 80
  4. lemma OAI.SLEExactGauge.Layer.DiskPair.injOn line 89
  5. lemma OAI.SLEExactGauge.Layer.DiskPair.inverse_derivative line 94
  6. lemma OAI.SLEExactGauge.Layer.DiskPair.deriv_ne_zero line 103
  7. lemma OAI.SLEExactGauge.Layer.DiskPair.second_derivative_zero line 108
  8. def OAI.SLEExactGauge.SlitMaps.diskAuto line 165
  9. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_den_ne line 167
  10. lemma OAI.SLEExactGauge.SlitMaps.disk_norm_identity line 178
  11. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_mapsTo line 185
  12. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_hasDerivAt line 194
  13. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_deriv line 204
  14. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_deriv_ne line 208
  15. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_injOn line 213
  16. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_self line 222
  17. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_zero line 224
  18. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_norm_deriv_zero line 226
  19. lemma OAI.SLEExactGauge.SlitMaps.diskAuto_norm_deriv_self line 234
  20. lemma OAI.SLEExactGauge.Layer.diskAuto_neg_inverse line 259
  21. lemma OAI.SLEExactGauge.Layer.DiskPair.recenter line 272
  22. lemma OAI.SLEExactGauge.Layer.diskAuto_deriv_zero_exact line 292
  23. lemma OAI.SLEExactGauge.Layer.diskAuto_second_zero line 297
  24. lemma OAI.SLEExactGauge.Layer.DiskPair.preSchwarzian line 316
  25. def OAI.SLEExactGauge.Layer.logRadius line 377
  26. lemma OAI.SLEExactGauge.Layer.DiskPair.logRadius_smooth line 380
  27. lemma OAI.SLEExactGauge.Layer.DiskPair.logRadius_laplacian line 387
  28. lemma OAI.SLEExactGauge.Layer.DiskPair.logRadius_gradient line 397
  29. lemma OAI.SLEExactGauge.Layer.DiskPair.logRadius_gradient_sq line 421
  30. def OAI.SLEExactGauge.Layer.layerProfile line 465
  31. def OAI.SLEExactGauge.Layer.layerProfileD line 467
  32. def OAI.SLEExactGauge.Layer.layerProfileDD line 469
  33. lemma OAI.SLEExactGauge.Layer.profile_smooth line 472
  34. lemma OAI.SLEExactGauge.Layer.profile_derivative line 478
  35. lemma OAI.SLEExactGauge.Layer.profile_second line 485
  36. lemma OAI.SLEExactGauge.Layer.profile_bounds line 494
  37. lemma OAI.SLEExactGauge.Layer.profileD_nonneg line 499
  38. lemma OAI.SLEExactGauge.Layer.profileDD_le line 503
  39. lemma OAI.SLEExactGauge.Layer.profileD_lower line 513
  40. def OAI.SLEExactGauge.Layer.layerExponent line 535
  41. lemma OAI.SLEExactGauge.Layer.layerExponent_bounds line 537
  42. def OAI.SLEExactGauge.Layer.shiftedRadius line 549
  43. def OAI.SLEExactGauge.Layer.layerBarrier line 551
  44. lemma OAI.SLEExactGauge.Layer.DiskPair.shifted_smooth line 554
  45. lemma OAI.SLEExactGauge.Layer.DiskPair.shifted_laplacian line 558
  46. lemma OAI.SLEExactGauge.Layer.shifted_fderiv line 566
  47. lemma OAI.SLEExactGauge.Layer.DiskPair.barrier_smooth line 569
  48. lemma OAI.SLEExactGauge.Layer.barrier_bounds line 575
  49. lemma OAI.SLEExactGauge.Layer.profile_laplacian_estimate line 581
  50. lemma OAI.SLEExactGauge.Layer.DiskPair.barrier_drop line 601
  51. lemma OAI.SLEExactGauge.Layer.DiskPair.barrier_superharmonic line 616
  52. lemma OAI.SLEExactGauge.Layer.DiskPair.shifted_exp line 624
  53. lemma OAI.SLEExactGauge.Layer.DiskPair.barrier_layer line 632
  54. lemma OAI.SLEExactGauge.Layer.radial_green_annulus line 667
  55. lemma OAI.SLEExactGauge.Layer.radial_green_integral line 734
  56. lemma OAI.SLEExactGauge.Layer.superharmonic_radial_green line 802
  57. theorem OAI.SLEExactGauge.Layer.superharmonic_disk_green line 837
  58. lemma OAI.SLEExactGauge.Layer.univalent_not_locally_constant line 889
  59. lemma OAI.SLEExactGauge.Layer.univalent_punctured_derivative line 901
  60. theorem OAI.SLEExactGauge.Layer.univalent_diskPair line 915