OAI/Probability/SLE/Loewner/RawDiskRadiusLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The disk variable on raw driver space has exactly the finite centered law used in the prescribed moment coefficients and tail budget.

  1. def OAI.SLEExactGauge.Multipoint.RawCanonicalMass.diskAtRadius line 17
  2. lemma OAI.SLEExactGauge.Multipoint.RawCanonicalMass.diskAtRadius_nonneg line 22
  3. lemma OAI.SLEExactGauge.Multipoint.RawCanonicalMass.diskAtRadius_measurable line 25
  4. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.raw_diskAtRadius_eq line 48
  5. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.raw_diskAtRadius_finiteCentered_tail line 59
  6. def OAI.SLEExactGauge.rawCenteredDiskLaw line 85
  7. lemma OAI.SLEExactGauge.rawCenteredDiskLaw_lintegral line 89
  8. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.raw_centeredDiskTail_eq line 112