OAI/Probability/SLELocalization/SobolevMeans.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Rectangle Energy estimates.

  1. theorem OAI.SLEExactGauge.RectangleEnergy.dyadic_weighted_energy line 17
  2. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicKernel_integral_mul line 27
  3. lemma OAI.SLEExactGauge.RectangleEnergy.dyadic_L1_telescoping line 44
  4. theorem OAI.SLEExactGauge.RectangleEnergy.critical_means_from_L1 line 56
  5. lemma OAI.SLEExactGauge.RectangleEnergy.rectangle_measure_restrict line 94
  6. lemma OAI.SLEExactGauge.RectangleEnergy.rectangle_measure_real line 105
  7. theorem OAI.SLEExactGauge.RectangleEnergy.strip_nested_means line 118
  8. lemma OAI.SLEExactGauge.RectangleEnergy.rectangle_measure_total line 176
  9. theorem OAI.SLEExactGauge.RectangleEnergy.strip_parent_energy line 183
  10. lemma OAI.SLEExactGauge.RectangleEnergy.rectangleProb_integral line 217
  11. theorem OAI.SLEExactGauge.RectangleEnergy.strip_negative_mean line 227
  12. structure OAI.SLEExactGauge.RectangleEnergy.DRect line 289
  13. def OAI.SLEExactGauge.RectangleEnergy.DRect.closed line 310
  14. def OAI.SLEExactGauge.RectangleEnergy.DRect.cells line 312
  15. def OAI.SLEExactGauge.RectangleEnergy.DRect.measure line 314
  16. def OAI.SLEExactGauge.RectangleEnergy.DRect.halfLo line 317
  17. def OAI.SLEExactGauge.RectangleEnergy.DRect.halfHi line 319
  18. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.half_bounds line 321
  19. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.half_length line 329
  20. def OAI.SLEExactGauge.RectangleEnergy.DRect.child line 332
  21. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.child_bounds line 340
  22. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.child_width line 346
  23. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.child_height line 348
  24. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.child_closed_subset line 350
  25. def OAI.SLEExactGauge.RectangleEnergy.DRect.chooseSide line 355
  26. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.mem_chosen_half line 357
  27. def OAI.SLEExactGauge.RectangleEnergy.DRect.chooseChild line 364
  28. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.mem_chosen_child line 367
  29. def OAI.SLEExactGauge.RectangleEnergy.DIndex line 385
  30. instance OAI.SLEExactGauge.RectangleEnergy.dIndex_fintype line 389
  31. def OAI.SLEExactGauge.RectangleEnergy.dyadicRect line 394
  32. def OAI.SLEExactGauge.RectangleEnergy.dParent line 398
  33. def OAI.SLEExactGauge.RectangleEnergy.dFromBits line 400
  34. lemma OAI.SLEExactGauge.RectangleEnergy.dFromBits_congr line 404
  35. def OAI.SLEExactGauge.RectangleEnergy.dExtendBits line 412
  36. lemma OAI.SLEExactGauge.RectangleEnergy.dFromBits_extend line 416
  37. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicRect_width line 428
  38. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicRect_height line 434
  39. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicRect_bounds line 440
  40. def OAI.SLEExactGauge.RectangleEnergy.dPointBranch line 450
  41. lemma OAI.SLEExactGauge.RectangleEnergy.dPointBranch_parent line 454
  42. lemma OAI.SLEExactGauge.RectangleEnergy.dPointBranch_mem line 457
  43. lemma OAI.SLEExactGauge.RectangleEnergy.probability_means_tendsto line 463
  44. lemma OAI.SLEExactGauge.RectangleEnergy.rectangle_point_dist line 482
  45. theorem OAI.SLEExactGauge.RectangleEnergy.strip_rectangle_means_tendsto line 492
  46. def OAI.SLEExactGauge.RectangleEnergy.stripMean line 537
  47. def OAI.SLEExactGauge.RectangleEnergy.stripEnergy line 541
  48. def OAI.SLEExactGauge.RectangleEnergy.rectCoefficient line 544
  49. lemma OAI.SLEExactGauge.RectangleEnergy.rectCoefficient_pos line 546
  50. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicRect_coefficient line 552
  51. theorem OAI.SLEExactGauge.RectangleEnergy.strip_dyadic_mean_critical line 575
  52. theorem OAI.SLEExactGauge.RectangleEnergy.strip_dyadic_mean_step line 602
  53. theorem OAI.SLEExactGauge.RectangleEnergy.strip_dyadic_mean_limit line 622
  54. def OAI.SLEExactGauge.RectangleEnergy.totalStripEnergy line 654
  55. lemma OAI.SLEExactGauge.RectangleEnergy.totalStripEnergy_nonneg line 658
  56. lemma OAI.SLEExactGauge.RectangleEnergy.totalStripEnergy_eq line 661
  57. theorem OAI.SLEExactGauge.RectangleEnergy.totalStripEnergy_bound line 683
  58. lemma OAI.SLEExactGauge.RectangleEnergy.stripEnergy_le_total line 695
  59. def OAI.SLEExactGauge.RectangleEnergy.unitSlab line 708
  60. def OAI.SLEExactGauge.RectangleEnergy.longSlab line 710
  61. def OAI.SLEExactGauge.RectangleEnergy.slabMeanCoefficient line 712
  62. lemma OAI.SLEExactGauge.RectangleEnergy.slabMeanCoefficient_pos line 714
  63. lemma OAI.SLEExactGauge.RectangleEnergy.longSlab_coefficient line 718
  64. theorem OAI.SLEExactGauge.RectangleEnergy.negative_unitSlab_mean line 729
  65. theorem OAI.SLEExactGauge.RectangleEnergy.positive_unitSlab_mean line 749
  66. lemma OAI.SLEExactGauge.RectangleEnergy.complex_rectangle_diff_norm line 798
  67. lemma OAI.SLEExactGauge.RectangleEnergy.exp_difference_small line 810
  68. def OAI.SLEExactGauge.RectangleEnergy.expCellScale line 817
  69. lemma OAI.SLEExactGauge.RectangleEnergy.expCellScale_pos line 819
  70. lemma OAI.SLEExactGauge.RectangleEnergy.expCellScale_ge line 821
  71. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicCell_exp_geometry line 826
  72. def OAI.SLEExactGauge.BoundaryCutoff.clamp line 883
  73. def OAI.SLEExactGauge.BoundaryCutoff.velocity line 885
  74. lemma OAI.SLEExactGauge.BoundaryCutoff.side_sq line 887
  75. lemma OAI.SLEExactGauge.BoundaryCutoff.clamp_eq line 892
  76. lemma OAI.SLEExactGauge.BoundaryCutoff.clamp_norm line 899
  77. lemma OAI.SLEExactGauge.BoundaryCutoff.clamp_ne_zero line 906
  78. lemma OAI.SLEExactGauge.BoundaryCutoff.clamp_norm_sub line 909
  79. lemma OAI.SLEExactGauge.BoundaryCutoff.velocity_eq line 924
  80. lemma OAI.SLEExactGauge.BoundaryCutoff.norm_velocity_le line 929