OAI/Probability/SLELocalization/DyadicKernels.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Rectangle Energy estimates.

  1. lemma OAI.SLEExactGauge.RectangleEnergy.annular_invSquare_integral line 16
  2. def OAI.SLEExactGauge.RectangleEnergy.annularKernel line 55
  3. lemma OAI.SLEExactGauge.RectangleEnergy.annularKernel_integral line 58
  4. lemma OAI.SLEExactGauge.RectangleEnergy.complex_real_jacobian line 87
  5. theorem OAI.SLEExactGauge.RectangleEnergy.conformal_truncation_energy line 92
  6. def OAI.SLEExactGauge.RectangleEnergy.sphereTruncation line 134
  7. lemma OAI.SLEExactGauge.RectangleEnergy.sphereTruncation_coe line 137
  8. lemma OAI.SLEExactGauge.RectangleEnergy.sphereTruncation_infty line 140
  9. lemma OAI.SLEExactGauge.RectangleEnergy.sphereTruncation_continuous line 143
  10. lemma OAI.SLEExactGauge.RectangleEnergy.sphereTruncation_bounds line 162
  11. lemma OAI.SLEExactGauge.RectangleEnergy.sphereTruncation_top_of_outside line 168
  12. def OAI.SLEExactGauge.RectangleEnergy.openStrip line 190
  13. def OAI.SLEExactGauge.RectangleEnergy.closedStrip line 192
  14. def OAI.SLEExactGauge.RectangleEnergy.stripPotential line 194
  15. lemma OAI.SLEExactGauge.RectangleEnergy.openStrip_isOpen line 197
  16. lemma OAI.SLEExactGauge.RectangleEnergy.exp_mem_halfPlane line 201
  17. lemma OAI.SLEExactGauge.RectangleEnergy.exp_mem_closedHalfPlane line 205
  18. lemma OAI.SLEExactGauge.RectangleEnergy.exp_injOn_strip line 209
  19. lemma OAI.SLEExactGauge.RectangleEnergy.stripPotential_continuous line 215
  20. theorem OAI.SLEExactGauge.RectangleEnergy.strip_potential_energy line 222
  21. theorem OAI.SLEExactGauge.RectangleEnergy.access_section_zero line 248
  22. lemma OAI.SLEExactGauge.RectangleEnergy.stripPotential_interior_eq line 271
  23. lemma OAI.SLEExactGauge.RectangleEnergy.stripPotential_vertical_AC_interior line 278
  24. lemma OAI.SLEExactGauge.RectangleEnergy.stripPotential_vertical_deriv line 302
  25. theorem OAI.SLEExactGauge.RectangleEnergy.stripPotential_vertical_zero_energy line 319
  26. lemma OAI.SLEExactGauge.RectangleEnergy.strip_energy_integrable line 356
  27. lemma OAI.SLEExactGauge.RectangleEnergy.strip_energy_integrable_prod line 366
  28. theorem OAI.SLEExactGauge.RectangleEnergy.strip_vertical_memLp_ae line 392
  29. theorem OAI.SLEExactGauge.RectangleEnergy.strip_negative_section_energy line 406
  30. lemma OAI.SLEExactGauge.RectangleEnergy.mean_difference_abs_le line 425
  31. theorem OAI.SLEExactGauge.RectangleEnergy.rectangle_mean_L1_bound line 442
  32. def OAI.SLEExactGauge.RectangleEnergy.intervalProb line 475
  33. lemma OAI.SLEExactGauge.RectangleEnergy.intervalProb_isProbability line 478
  34. lemma OAI.SLEExactGauge.RectangleEnergy.integral_intervalProb line 483
  35. lemma OAI.SLEExactGauge.RectangleEnergy.intervalProb_ae line 488
  36. lemma OAI.SLEExactGauge.RectangleEnergy.integrable_intervalProb line 492
  37. lemma OAI.SLEExactGauge.RectangleEnergy.intervalProb_integral_subinterval line 496
  38. lemma OAI.SLEExactGauge.RectangleEnergy.acl_line_L1 line 518
  39. theorem OAI.SLEExactGauge.RectangleEnergy.rectangle_poincare_L1 line 547
  40. lemma OAI.SLEExactGauge.RectangleEnergy.stripPotential_horizontal_AC line 627
  41. lemma OAI.SLEExactGauge.RectangleEnergy.stripPotential_horizontal_deriv line 649
  42. lemma OAI.SLEExactGauge.RectangleEnergy.stripPotential_vertical_AC line 666
  43. theorem OAI.SLEExactGauge.RectangleEnergy.strip_coordinate_ACL line 692
  44. lemma OAI.SLEExactGauge.RectangleEnergy.strip_gradient_rect_memLp line 731
  45. lemma OAI.SLEExactGauge.RectangleEnergy.strip_potential_rect_integrable line 751
  46. lemma OAI.SLEExactGauge.RectangleEnergy.strip_potential_mean_integrable line 768
  47. theorem OAI.SLEExactGauge.RectangleEnergy.strip_rectangle_poincare line 779
  48. lemma OAI.SLEExactGauge.RectangleEnergy.dyadic_subsum_le line 804
  49. lemma OAI.SLEExactGauge.RectangleEnergy.dyadic_subsum_square line 816
  50. def OAI.SLEExactGauge.RectangleEnergy.dyadicKernel line 844
  51. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicKernel_memLp line 847
  52. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicKernel_square_energy line 857