OAI/Probability/SLE/Geometry/RestartHalfPlaneGreen.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Half-plane form of the inverse-map Green covariance, including tests that reach the old trace. The current Green density vanishes off survival.

  1. def OAI.SLEExactGauge.Multipoint.extendHalfPlaneENN line 15
  2. lemma OAI.SLEExactGauge.Multipoint.extendHalfPlaneENN_apply line 18
  3. def OAI.SLEExactGauge.Multipoint.halfPlaneInversePoint line 21
  4. lemma OAI.SLEExactGauge.Multipoint.currentGreen_measurable line 28
  5. lemma OAI.SLEExactGauge.Multipoint.halfPlane_realDensity_lintegral line 37
  6. theorem OAI.SLEExactGauge.Multipoint.restart_halfPlane_green_test line 57