OAI/Probability/SLE/Mass/LevelStoppingMeasures.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The unreached part of a finite-level approximation at an arbitrary stopping time, as a positive measure.

  1. lemma OAI.SLEExactGauge.Multipoint.levelApproximationDensity_random_time_joint_measurable line 15
  2. lemma OAI.SLEExactGauge.Multipoint.halfPlaneLevelMeasure_random_time_measurable line 27
  3. def OAI.SLEExactGauge.Multipoint.halfPlaneStoppingRemainderMeasure line 42
  4. def OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure line 47
  5. def OAI.SLEExactGauge.Multipoint.halfPlaneStoppingGreenMeasure line 52
  6. lemma OAI.SLEExactGauge.Multipoint.stoppingGreen_joint_measurable line 57
  7. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingGreenMeasure_measurable line 68
  8. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingRemainderMeasure_measurable line 82
  9. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure_measurable line 96
  10. lemma OAI.SLEExactGauge.Multipoint.halfPlaneLevelMeasure_stopping_split line 110
  11. theorem OAI.SLEExactGauge.Multipoint.halfPlaneStoppingRemainderMeasure_conditional_mean line 132
  12. theorem OAI.SLEExactGauge.Multipoint.halfPlaneLevelMeasure_stopping_conditional_split line 160
  13. theorem OAI.SLEExactGauge.Multipoint.halfPlaneStoppingGreenMeasure_mean_le line 189
  14. theorem OAI.SLEExactGauge.Multipoint.stoppingCurrentGreen_spatial_mean_tendsto line 218
  15. theorem OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure_mean_tendsto line 256