OAI/Probability/SLE/Loewner/UnivalentMovingNormalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Moving normalizations in a compact subset of the half-plane give a locally bounded subsequence, using the coarse Bloch estimate.

  1. lemma OAI.SLEExactGauge.univalent_moving_normalization_subsequence line 13