OAI/Probability/SLE/Mass/CountableLevelKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual common Radon limits with their exact conditional kernels at any prescribed countable set of deterministic times.

  1. def OAI.SLEExactGauge.Multipoint.levelMassTimes line 18
  2. lemma OAI.SLEExactGauge.Multipoint.levelMassTimes_zero line 22
  3. lemma OAI.SLEExactGauge.Multipoint.levelMassTimes_succ line 23
  4. theorem OAI.SLEExactGauge.Multipoint.exists_countable_level_radon_kernels line 25