OAI/Probability/SLE/NestedMeans.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Nested Means for chordal SLE.

  1. lemma OAI.SLEExactGauge.slice_oscillation_le_integral line 14
  2. lemma OAI.SLEExactGauge.locallyLipschitz_ae_differentiable line 58
  3. def OAI.SLEExactGauge.complexCoordinates line 78
  4. lemma OAI.SLEExactGauge.complexCoordinates_eq line 80
  5. lemma OAI.SLEExactGauge.complexCoordinates_preserving line 84
  6. lemma OAI.SLEExactGauge.complexCoordinates_continuous line 88
  7. lemma OAI.SLEExactGauge.vertical_isometry line 92
  8. lemma OAI.SLEExactGauge.horizontal_isometry line 100
  9. lemma OAI.SLEExactGauge.locallyLipschitz_comp_of_isometry line 105
  10. lemma OAI.SLEExactGauge.vertical_deriv_norm_le line 114
  11. lemma OAI.SLEExactGauge.horizontal_deriv_norm_le line 126
  12. def OAI.SLEExactGauge.cartesianRectangle line 138
  13. lemma OAI.SLEExactGauge.cartesianRectangle_preimage line 141
  14. lemma OAI.SLEExactGauge.cartesianRectangle_measurable line 147
  15. lemma OAI.SLEExactGauge.complexCoordinates_rect_preserving line 152
  16. lemma OAI.SLEExactGauge.cartesianRectangle_compact line 163
  17. lemma OAI.SLEExactGauge.cartesianRectangle_integral line 176
  18. def OAI.SLEExactGauge.fullOpenStrip line 186
  19. def OAI.SLEExactGauge.fullClosedStrip line 187
  20. lemma OAI.SLEExactGauge.fullOpenStrip_isOpen line 189
  21. lemma OAI.SLEExactGauge.cartesianRectangle_ae_strip line 193
  22. lemma OAI.SLEExactGauge.cartesianRectangle_volume line 206
  23. lemma OAI.SLEExactGauge.unitSlab_norm_integral_le line 213
  24. lemma OAI.SLEExactGauge.vertical_derivative_bound_ae line 230
  25. lemma OAI.SLEExactGauge.negativeSlab_mean_le line 243
  26. lemma OAI.SLEExactGauge.interval_unit_mean_comparison line 298
  27. lemma OAI.SLEExactGauge.cartesianRectangle_integral_symm line 327
  28. lemma OAI.SLEExactGauge.horizontal_derivative_bound_ae line 337
  29. lemma OAI.SLEExactGauge.slab_integral_comparison line 351
  30. lemma OAI.SLEExactGauge.rectangle_energy_le_total line 401
  31. lemma OAI.SLEExactGauge.rectangle_norm_integral_le line 409
  32. lemma OAI.SLEExactGauge.negativeSlab_mean_small line 428
  33. lemma OAI.SLEExactGauge.positiveSlab_mean_small line 446
  34. def OAI.SLEExactGauge.SourceSlabSmallMeanTarget line 478
  35. theorem OAI.SLEExactGauge.sourceSlabSmallMean line 489
  36. def OAI.SLEExactGauge.closedIntegerStrip line 501
  37. def OAI.SLEExactGauge.openIntegerStrip line 504
  38. lemma OAI.SLEExactGauge.complex_re_fiber_null line 507
  39. lemma OAI.SLEExactGauge.complex_im_fiber_null line 512
  40. lemma OAI.SLEExactGauge.closedIntegerStrip_ae_open line 517
  41. lemma OAI.SLEExactGauge.openIntegerStrip_isOpen line 536
  42. lemma OAI.SLEExactGauge.openIntegerStrip_disjoint line 542
  43. def OAI.SLEExactGauge.slabShift line 552
  44. lemma OAI.SLEExactGauge.slabShift_continuous line 554
  45. lemma OAI.SLEExactGauge.slabShift_isometry line 558
  46. lemma OAI.SLEExactGauge.slabShift_preimage_closed line 561
  47. lemma OAI.SLEExactGauge.slabShift_preimage_open line 568
  48. lemma OAI.SLEExactGauge.slabShift_preserving_open line 574
  49. lemma OAI.SLEExactGauge.slabShift_preserving_closed line 581
  50. lemma OAI.SLEExactGauge.gradient_comp_slabShift line 588
  51. lemma OAI.SLEExactGauge.slabShift_integral line 592
  52. lemma OAI.SLEExactGauge.slabShift_energy line 597
  53. lemma OAI.SLEExactGauge.slabShift_mem_strip line 604
  54. lemma OAI.SLEExactGauge.slabShift_locallyLipschitz line 608
  55. lemma OAI.SLEExactGauge.slabShift_gradient_memLp line 619
  56. lemma OAI.SLEExactGauge.slabShift_source_weakGradient line 629
  57. lemma OAI.SLEExactGauge.integerSlab_energy_budget line 642
  58. lemma OAI.SLEExactGauge.abstract_slab_exponential_budget line 663
  59. def OAI.SLEExactGauge.SourceStripLocalizationTarget line 710
  60. lemma OAI.SLEExactGauge.stripRectangle_zero_eq_cartesian line 728
  61. lemma OAI.SLEExactGauge.slabShift_average line 733
  62. lemma OAI.SLEExactGauge.slabShift_dyadic line 742
  63. lemma OAI.SLEExactGauge.slabShift_continuousOn line 749
  64. lemma OAI.SLEExactGauge.point_integer_slab line 757
  65. lemma OAI.SLEExactGauge.slab_energy_le_total line 766
  66. theorem OAI.SLEExactGauge.sourceStripLocalization line 774