OAI/Probability/SLE/Mass/LevelRandomRadon.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measurable versions and simultaneous time ordering of the actual common Radon limits.

  1. lemma OAI.SLEExactGauge.Multipoint.halfPlaneLevelMeasure_mono line 18
  2. lemma OAI.SLEExactGauge.Multipoint.convexLevelMeasure_mono line 28
  3. lemma OAI.SLEExactGauge.Multipoint.convexLevelMeasure_test_measurable line 40
  4. theorem OAI.SLEExactGauge.Multipoint.exists_measurable_level_radon_limits line 59