OAI/Probability/SLE/Mass/LevelStoppingGreenLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Increasing finite radius levels recover the Green kernel killed at an arbitrary stopping time. Its expectation is bounded by the initial Green function, also when the stopping time may be infinite.

  1. def OAI.SLEExactGauge.Multipoint.stoppingGreen line 16
  2. lemma OAI.SLEExactGauge.Multipoint.levelStoppingCurrentGreen_mono line 22
  3. lemma OAI.SLEExactGauge.Multipoint.levelStoppingCurrentGreen_eventually_eq line 37
  4. theorem OAI.SLEExactGauge.Multipoint.levelStoppingCurrentGreen_mean_le line 53
  5. theorem OAI.SLEExactGauge.Multipoint.stoppingGreen_mean_le line 89