OAI/Probability/SLE/Loewner/TargetSurvivalLifetime.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every raw point lost by a finite time has a positive finite lifetime, and survives precisely the earlier nonnegative times.

  1. lemma OAI.SLEExactGauge.Target.surviving_zero line 16
  2. theorem OAI.SLEExactGauge.Target.exists_survival_lifetime line 22