OAI/Probability/SLE/Mass/DiskLevelMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Centered level moments in the prescribed physical disk. The radius cap and spatial kernel are independent of the chart angle.

  1. def OAI.SLEExactGauge.Multipoint.diskStoppedGreen line 16
  2. def OAI.SLEExactGauge.Multipoint.diskLevelMass line 22
  3. def OAI.SLEExactGauge.Multipoint.diskCenterHit line 27
  4. lemma OAI.SLEExactGauge.Multipoint.diskStoppedGreen_nonneg line 32
  5. lemma OAI.SLEExactGauge.Multipoint.measurable_diskStoppedGreen line 38
  6. lemma OAI.SLEExactGauge.Multipoint.measurableSet_diskCenterHit line 53
  7. theorem OAI.SLEExactGauge.Multipoint.diskStoppedGreen_centered_product_bound line 72