OAI/Probability/SLE/Geometry/CenteredDiskLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite centered law with the prescribed initial angle mixture. Its moments are exactly the finite coefficients in the gauge construction.

  1. def OAI.SLEExactGauge.centeredDiskDensity line 18
  2. def OAI.SLEExactGauge.centeredDiskLaw line 22
  3. lemma OAI.SLEExactGauge.centeredDiskDensity_measurable line 27
  4. lemma OAI.SLEExactGauge.centeredDiskLaw_lintegral line 38
  5. lemma OAI.SLEExactGauge.centeredDiskLaw_isProbability line 72
  6. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.centeredDiskLaw_moment line 100