OAI/Analysis/LipschitzHilbert/Estimates/RelativeExitIntervals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every sufficiently large interval crosses a relative exit whose jump controls that interval. This is the finite, initial-value-radius version of Zorin-Kranich, Bernoulli 26 (2020), Lemma 2.2.

  1. theorem OAI.LipschitzHilbert.relativeExitTimes_last line 13
  2. theorem OAI.LipschitzHilbert.runningOscillation_at_last_exit line 28
  3. theorem OAI.LipschitzHilbert.relative_interval_crosses_exit line 53