OAI/Probability/SLE/Loewner/InverseSmallSemicircles.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Arbitrarily small closed image semicircles at each real boundary point. The endpoint values are obtained from finite energy, not from an assumed continuous extension of the inverse map.

  1. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.inverse_log_holomorphic line 16
  2. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.exists_small_inverse_semicircle line 27