OAI/Probability/SLE/Mass/RationalTraceMassProgressiveVersion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A single reconstruction from rational left samples is progressive in the uncompleted filtration and agrees at every time on the common good set.

  1. def OAI.SLEExactGauge.leftRationalSample line 19
  2. lemma OAI.SLEExactGauge.leftRationalSample_nonneg line 22
  3. lemma OAI.SLEExactGauge.leftRationalSample_le line 26
  4. lemma OAI.SLEExactGauge.leftRationalSample_tendsto line 32
  5. lemma OAI.SLEExactGauge.leftRationalSample_measurable line 39
  6. def OAI.SLEExactGauge.rationalRadonExtension line 43
  7. theorem OAI.SLEExactGauge.rationalRadonExtension_regular line 47
  8. theorem OAI.SLEExactGauge.rationalRadonExtension_progressive line 56
  9. theorem OAI.SLEExactGauge.rationalRadonExtension_common_version line 92