OAI/Probability/SLE/Mass/LevelStoppingKernel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite-level remaining Green kernel at any Brownian stopping time. Both sides vanish at an infinite stopping time. Finite cutoffs use the existing optional identity for the stopped Green martingale.

  1. def OAI.SLEExactGauge.Multipoint.levelStoppingRemainderGreen line 17
  2. def OAI.SLEExactGauge.Multipoint.levelStoppingCurrentGreen line 23
  3. lemma OAI.SLEExactGauge.Multipoint.levelStoppingRemainderGreen_nonneg line 29
  4. lemma OAI.SLEExactGauge.Multipoint.levelStoppingCurrentGreen_nonneg line 40
  5. theorem OAI.SLEExactGauge.Multipoint.levelStoppingRemainderGreen_finite_condExp line 51
  6. theorem OAI.SLEExactGauge.Multipoint.levelStoppingRemainderGreen_finite_setLIntegral line 110
  7. lemma OAI.SLEExactGauge.Multipoint.stopped_setLIntegral_cutoffs line 140
  8. theorem OAI.SLEExactGauge.Multipoint.levelStoppingRemainderGreen_setLIntegral line 174