OAI/Probability/SLE/Loewner/VanishingHeightRealLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

At a finite lifetime, vanishing height and continuity of the driver force the forward real coordinate to approach the driver.

  1. theorem OAI.SLEExactGauge.forward_real_tendsto_driver_of_height_zero line 13