OAI/Probability/SLE/Mass/HalfPlaneLevelMeasures.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite-level approximants as locally finite measures on the open half-plane, and their signed compact tests viewed on the ambient plane.

  1. lemma OAI.SLEExactGauge.Multipoint.levelMass_lt_top_of_compact line 14
  2. def OAI.SLEExactGauge.Multipoint.halfPlaneLevelMeasure line 37
  3. theorem OAI.SLEExactGauge.Multipoint.halfPlaneLevelMeasure_finite_on_compacts line 42
  4. def OAI.SLEExactGauge.Multipoint.extendHalfPlaneTest line 58
  5. lemma OAI.SLEExactGauge.Multipoint.extendHalfPlaneTest_apply line 61
  6. lemma OAI.SLEExactGauge.Multipoint.extendHalfPlaneTest_of_not_mem line 64
  7. lemma OAI.SLEExactGauge.Multipoint.extendHalfPlaneTest_measurable line 70
  8. lemma OAI.SLEExactGauge.Multipoint.extendHalfPlaneTest_support line 74
  9. lemma OAI.SLEExactGauge.Multipoint.extendHalfPlaneTest_norm_le line 83
  10. lemma OAI.SLEExactGauge.Multipoint.integral_halfPlaneLevelMeasure line 93