OAI/Probability/SLE/Mass/LevelCurrentLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Increasing finite-level remaining kernels converge to the actual killed Green kernel, also after averaging on an arbitrary event.

  1. def OAI.SLEExactGauge.Multipoint.halfPlaneGreenMeasure line 15
  2. lemma OAI.SLEExactGauge.Multipoint.halfPlaneGreenMeasure_measurable line 21
  3. lemma OAI.SLEExactGauge.Multipoint.levelCurrentGreen_le_green line 34
  4. lemma OAI.SLEExactGauge.Multipoint.halfPlaneCurrentMeasure_le_green line 47
  5. theorem OAI.SLEExactGauge.Multipoint.currentGreen_spatial_mean_tendsto line 60
  6. theorem OAI.SLEExactGauge.Multipoint.halfPlaneCurrentMeasure_mean_tendsto line 98
  7. theorem OAI.SLEExactGauge.Multipoint.halfPlaneGreenMeasure_mean_le line 118