OAI/Probability/SLE/Loewner/TargetInverseExistence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reverse flow supplies every point of the upper half-plane as an image of the raw surviving flow, for every continuous based driver.

  1. lemma OAI.SLEExactGauge.reverseField_im_nonneg line 14
  2. theorem OAI.SLEExactGauge.Target.reverse_trajectory_preimage line 26
  3. theorem OAI.SLEExactGauge.Target.exists_surviving_preimage line 74