OAI/Probability/SLE/Loewner/VanishingHeightRealBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Vanishing forward height forces the real coordinate to remain between the future driver bounds.

  1. lemma OAI.SLEExactGauge.forward_height_lower_of_real_gap line 14
  2. theorem OAI.SLEExactGauge.real_le_future_driver_bound_of_height_zero line 34
  3. theorem OAI.SLEExactGauge.future_driver_lower_le_real_of_height_zero line 76