PlanarPassageNeighborhood.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Passage neighborhoods in the entire physical plane. Recentring a physical ribbon does not preserve the upper half-plane, and this construction uses only its embedded coordinate patch.

theorem OAI.SLEExactGauge.RibbonCoordinates.limiting_guide_passage_neighborhood_plane line 17

Source documentation

The actual limiting guide supplies a common physical neighborhood and all varying-region conditions used by the retained-mass passage theorem.

theorem limiting_guide_passage_neighborhood_plane
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K : Set ℂ) (C L : ℝ≥0)
    (hC : 0 < C) (hL : 0 < L)
    (hupper : ∀ n, LipschitzOnWith C (Pₙ n) K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hP : ContinuousOn P K)
    (α : ℝ → ℂ) (hα : ContinuousOn α (Icc 0 2)) (x ε η : ℝ)
    (hx : |x| < ε) (hη : 0 < η)
    (hshape : EqOn α (fun t => P (guideCoordinate 0 x t)) (Icc 0 2))
    (hmem : ∀ t ∈ Icc (0 : ℝ) (3 / 2), guideCoordinate 0 x t ∈ interior K)
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate