OAI/Probability/SLE/Mass/LevelRemainderMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The unreached part of a finite-level approximation, as a positive measure. The conditional Green identity holds as a measure identity.

  1. def OAI.SLEExactGauge.Multipoint.halfPlaneRemainderMeasure line 15
  2. def OAI.SLEExactGauge.Multipoint.halfPlaneCurrentMeasure line 20
  3. lemma OAI.SLEExactGauge.Multipoint.levelDensity_split line 25
  4. lemma OAI.SLEExactGauge.Multipoint.halfPlaneRemainderMeasure_measurable line 37
  5. lemma OAI.SLEExactGauge.Multipoint.halfPlaneCurrentMeasure_measurable line 51
  6. lemma OAI.SLEExactGauge.Multipoint.halfPlaneLevelMeasure_split line 65
  7. theorem OAI.SLEExactGauge.Multipoint.halfPlaneRemainderMeasure_conditional_mean line 83