OAI/Probability/SLE/Loewner/TargetCutoffTrajectory.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The Euler-defined cutoff agrees with every classical trajectory on a compact time interval. Positive height makes the cutoff inactive.

  1. lemma OAI.SLEExactGauge.Target.cutoffFlow_eq_of_trajectory line 14
  2. lemma OAI.SLEExactGauge.Target.cutoffFlow_continuousOn line 29
  3. lemma OAI.SLEExactGauge.Target.cutoffFlow_hasDerivWithinAt line 35
  4. lemma OAI.SLEExactGauge.Target.cutoffFlow_zero line 46
  5. lemma OAI.SLEExactGauge.Target.cutoff_inactive_of_height line 51
  6. lemma OAI.SLEExactGauge.Target.cutoffFlow_eq_of_positive_trajectory line 68
  7. lemma OAI.SLEExactGauge.Target.surviving_cutoff_height line 82
  8. lemma OAI.SLEExactGauge.Target.surviving_of_positive_trajectory line 93