OAI/Probability/SLELocalization/ConformalLocalization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Rectangle Energy estimates.

  1. theorem OAI.SLEExactGauge.RectangleEnergy.strip_slab_half_mean line 15
  2. lemma OAI.SLEExactGauge.RectangleEnergy.unitSlab_cells_disjoint line 64
  3. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.measure_eq_restrict line 77
  4. theorem OAI.SLEExactGauge.RectangleEnergy.strip_slab_energy_sum line 82
  5. lemma OAI.SLEExactGauge.RectangleEnergy.energy_exp_linearize line 131
  6. theorem OAI.SLEExactGauge.RectangleEnergy.energy_event_union line 150
  7. def OAI.SLEExactGauge.RectangleEnergy.logEnergyExit line 189
  8. lemma OAI.SLEExactGauge.RectangleEnergy.rectCoefficient_unitSlab line 194
  9. theorem OAI.SLEExactGauge.RectangleEnergy.logTrace_localization line 201
  10. def OAI.SLEExactGauge.conformalExit line 278
  11. lemma OAI.SLEExactGauge.norm_le_of_pre_modulus line 283
  12. lemma OAI.SLEExactGauge.conformalExit_logEnergyExit line 293
  13. theorem OAI.SLEExactGauge.uniform_conformal_localization line 323