OAI/Probability/SLE/Mass/LevelStoppingTests.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Signed compact-test convergence for the Green remainder at arbitrary stopping times, and its preservation by the chosen convex tails.

  1. lemma OAI.SLEExactGauge.Multipoint.levelStoppingCurrentGreen_le_green line 18
  2. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure_le_green line 36
  3. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure_mean_lintegral_test line 50
  4. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingGreenMeasure_mean_lintegral_test line 65
  5. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure_mean_lintegral_test_tendsto line 79
  6. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure_mean_le line 97
  7. theorem OAI.SLEExactGauge.Multipoint.halfPlaneStoppingCurrentMeasure_mean_test_tendsto line 116