OAI/Probability/SLELocalization/ConditionalAngles.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Finite Tilt estimates.

  1. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.target_setIntegral_le line 21
  2. theorem OAI.SLEExactGauge.LoewnerLocalized.localized_sum_tendsto line 114
  3. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.retarget_setIntegral line 214
  4. lemma OAI.SLEExactGauge.FiniteTilt.eventually_value_at_radius_general line 313
  5. lemma OAI.SLEExactGauge.FiniteTilt.tendsto_value_killed_general line 339
  6. lemma OAI.SLEExactGauge.FiniteTilt.tendsto_setLIntegral_value line 386
  7. theorem OAI.SLEExactGauge.finiteStoppedDensity_consistent line 440
  8. theorem OAI.SLEExactGauge.conditionalRadiusApproachBound line 470
  9. theorem OAI.SLEExactGauge.conditionalCenteredInverseAngleBound line 566