OAI/Probability/SLELocalization/Charge.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Charge estimates.

  1. def OAI.SLEExactGauge.sausage line 81
  2. def OAI.SLEExactGauge.sausageCharge line 84
  3. lemma OAI.SLEExactGauge.sausage_open line 87
  4. lemma OAI.SLEExactGauge.sausage_eq_dense line 94
  5. lemma OAI.SLEExactGauge.measurable_sausage_representative line 110
  6. lemma OAI.SLEExactGauge.expected_sausage_area line 128
  7. lemma OAI.SLEExactGauge.IsChordalSLE.maps line 279
  8. lemma OAI.SLEExactGauge.IsChordalSLE.continuous line 296
  9. lemma OAI.SLEExactGauge.IsChordalSLE.no_sausage_below line 302
  10. theorem OAI.SLEExactGauge.sausage_point_bound line 318
  11. def OAI.SLEExactGauge.regionBand line 559
  12. lemma OAI.SLEExactGauge.regionBand_measurable line 562
  13. lemma OAI.SLEExactGauge.lintegral_regionBand line 565
  14. lemma OAI.SLEExactGauge.volume_regionBand line 577
  15. lemma OAI.SLEExactGauge.height_kernel_finite line 582
  16. lemma OAI.SLEExactGauge.expected_sausage_area_bound line 726
  17. theorem OAI.SLEExactGauge.uniformBoundedRegionCharge line 779