OAI/Probability/SLE/Loewner/RawDiskAngleTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite centered disk success probability is a measurable function of its initial angle, so it can be tested against the actual angle law.

  1. def OAI.SLEExactGauge.Multipoint.RawCanonicalMass.angleDiskTail line 15
  2. lemma OAI.SLEExactGauge.Multipoint.RawCanonicalMass.angleDiskTail_measurable line 20
  3. lemma OAI.SLEExactGauge.Multipoint.RawCanonicalMass.angleDiskTail_average line 46