OAI/Probability/SLE/Geometry/CenteredDiskCoefficient.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The exact prescribed coefficient is a stopped canonical-mass moment under the finite centered law, including paths with an infinite level time.
- lemma
OAI.SLEExactGauge.Multipoint.CanonicalMass.diskScalar_progressiveline 21 - lemma
OAI.SLEExactGauge.Multipoint.CanonicalMass.normalizedStoppedDisk_eq_finiteline 30 - lemma
OAI.SLEExactGauge.Multipoint.CanonicalMass.levelCoefficient_eq_centered_momentline 52