OAI/Probability/SLE/Geometry/FirstDomainExit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual first exits forced by the waypoint route. Compactness of the finite time window gives an attained first exit, strictly after the early surviving prefix. No stopping-time or exit-location assumption is used.

  1. theorem OAI.SLEExactGauge.CrosscutSides.exists_first_domain_exit line 16
  2. theorem OAI.SLEExactGauge.CrosscutSides.first_domain_exit_unique line 37
  3. theorem OAI.SLEExactGauge.CrosscutSides.waypoint_first_exit_after_early_prefix line 48
  4. theorem OAI.SLEExactGauge.CrosscutSides.exit_prefix_positive line 63

    Source documentation

    A continuous nonzero side-coordinate cannot change sign before exit.

    theorem exit_prefix_positive
    {X : Type*} [TopologicalSpace X] {D : Set X} (j : X → ℝ)
    (hj : ContinuousOn j D) (ζ : ℝ → X) {a τ : ℝ}
    (hc : ContinuousOn ζ (Ico a τ)) (hin : MapsTo ζ (Ico a τ) D)
    (hn : ∀ t ∈ Ico a τ, j (ζ t) ≠ 0) (haτ : a < τ)
    (hstart : 0 < j (ζ a)) : ∀ t ∈ Ico a τ, 0 < j (ζ t) :=
…
  5. theorem OAI.SLEExactGauge.CrosscutSides.exit_prefix_negative line 72