OAI/Probability/SLE/Gauge/PrescribedRadiusLevels.lean
5 declarations, 0 contain sorry, 0 declared as axioms
Physical logarithmic levels for the exact prescribed radii. Uniformity includes moving centers down to height exp(-n).
- def
OAI.SLEExactGauge.Target.entryPhysicalLevelline 14 - lemma
OAI.SLEExactGauge.Target.entryPhysicalLevel_radiusline 18 - lemma
OAI.SLEExactGauge.Target.entryPhysicalLevel_gapline 30 - lemma
OAI.SLEExactGauge.Target.entryPhysicalLevel_cleanup_gapline 45 - lemma
OAI.SLEExactGauge.Target.eventually_entryPhysicalLevel_largeline 55