OAI/Probability/SLE/Loewner/LoewnerVerticalLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The zero-driver inverse trajectory, and convergence to it on the imaginary axis under a uniform perturbation of the driving function.

  1. def OAI.SLEExactGauge.verticalReversePath line 13
  2. lemma OAI.SLEExactGauge.verticalReversePath_zero line 15
  3. lemma OAI.SLEExactGauge.verticalReversePath_derivative line 19
  4. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.inverse_vertical_approximation line 46
  5. theorem OAI.SLEExactGauge.inverse_vertical_tendsto line 58