OAI/Probability/SLE/Geometry/PublishedCrosscutStraightening.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The relative half-plane proper-arc consequence of the published Jordan--Schönflies theorem. Reference: C. Thomassen, The Jordan-Schönflies Theorem and the Classification of Surfaces, Amer. Math. Monthly 99 (1992), 116--130, Theorem 3.1, p. 123, DOI 10.1080/00029890.1992.11995820.

The consequence used here is obtained by compactifying at infinity and applying the extension theorem to the two Jordan curves consisting of the proper arc and each real half-axis; the two extensions agree on their common arc and glue. The real boundary is prescribed pointwise. We parameterize this precise topological input explicitly. It contains no SLE, ribbon, Brownian probability, harmonic measure or angle estimate.

  1. def OAI.SLEExactGauge.PublishedHalfPlaneCrosscutStraightening line 23
  2. theorem OAI.SLEExactGauge.CrosscutSides.straightened_real_zero_iff line 35

    Source documentation

    Straightening identifies the entire interior zero set, including nonlocal pieces of the original access guide.

    theorem straightened_real_zero_iff
    (β : ℝ≥0 → ℂ) (h : ℂ ≃ₜ ℂ)
    (hH : MapsTo h upperHalfPlane upperHalfPlane)
    (hβ : ∀ t : ℝ≥0, h (β t) = (t : ℂ) * Complex.I)
    {z : ℂ} (hz : z ∈ upperHalfPlane) :
    (h z).re = 0 ↔ ∃ t : ℝ≥0, 0 < t ∧ β t = z := by
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane

  3. theorem OAI.SLEExactGauge.CrosscutSides.straightening_preserves_real_exit_limit line 54