OAI/Probability/SLE/Loewner/ReverseSmoothBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary barriers for the reverse Loewner equation with a bounded derivative of the driving function. The estimates are uniform in the positive starting height.

  1. lemma OAI.SLEExactGauge.damped_real_barrier line 14
  2. lemma OAI.SLEExactGauge.damped_real_abs_barrier line 37
  3. lemma OAI.SLEExactGauge.reverse_height_square_barrier line 53