OAI/Probability/SLE/Mass/CompactEntryLevels.lean
3 declarations, 0 contain sorry, 0 declared as axioms
Uniform control of the prescribed logarithmic levels on a compact subset of the open half-plane.
- lemma
OAI.SLEExactGauge.Target.continuous_entryPhysicalLevelline 13 - lemma
OAI.SLEExactGauge.Target.entryPhysicalLevel_bounded_on_compactline 21 - lemma
OAI.SLEExactGauge.Target.eventually_entryPhysicalLevel_large_on_compactline 28