OAI/Probability/SLELocalization/FiniteTimeMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Finite Time Mass estimates.

  1. theorem OAI.SLEExactGauge.physicalDistanceStoppedDensity line 18
  2. lemma OAI.SLEExactGauge.FiniteTilt.physicalValue_aemeasurable_tendsto line 71
  3. lemma OAI.SLEExactGauge.FiniteTilt.tendsto_setLIntegral_physicalValue line 91
  4. lemma OAI.SLEExactGauge.physical_radial_avoidance_identity line 130
  5. lemma OAI.SLEExactGauge.physicalStoppedDensity_aemeasurable line 158
  6. lemma OAI.SLEExactGauge.physicalStoppedDensity_pos_iff line 187
  7. lemma OAI.SLEExactGauge.physical_avoidance_at_finite_hit line 208
  8. lemma OAI.SLEExactGauge.physical_before_deep_radius line 224
  9. lemma OAI.SLEExactGauge.physical_early_nullMeasurable line 237
  10. theorem OAI.SLEExactGauge.finiteTimePhysicalDensity line 262