RibbonLimitPassageGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Deterministic ribbon regions used by the limiting splice. The envelope extends beyond the attained front, while its front slice is narrowed to supply the prescribed physical terminal tolerance.

def OAI.SLEExactGauge.RibbonCoordinates.passageCoordinateRegion line 15
def OAI.SLEExactGauge.RibbonCoordinates.physicalPassageRegion line 19
theorem OAI.SLEExactGauge.RibbonCoordinates.passageCoordinateRegion_isOpen line 22
theorem OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate_mem_passageRegion line 32
Source documentation
The prescribed access guide stays in the envelope, with its entire late part on the centerline, independently of the terminal tolerance.
```
theorem guideCoordinate_mem_passageRegion
    (C : ℝ≥0) (hC : 0 < C) {ε η x t : ℝ}
    (hx : |x| < ε) (hη : 0 < η) (ht : t ∈ Icc (0 : ℝ) (3 / 2)) :
    guideCoordinate 0 x t ∈ passageCoordinateRegion C ε η := by
…
```
Mentions: OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate, OAI.SLEExactGauge.RibbonCoordinates.passageCoordinateRegion

theorem OAI.SLEExactGauge.RibbonCoordinates.physicalPassageRegion_terminal line 51

Source documentation

The thin front slice gives the terminal physical tolerance required by FrontSuccess, using the actual upper patch Lipschitz constant.

theorem physicalPassageRegion_terminal
    (P : ℂ → ℂ) (K : Set ℂ) (C L : ℝ≥0) (ε η : ℝ)
    (hC : 0 < C) (hupper : LipschitzOnWith C P K)
    (hlower : ∀ x ∈ K, ∀ y ∈ K, dist x y ≤ L * dist (P x) (P y))
    (hbase : (1 : ℂ) ∈ K) {z : ℂ}
    (hz : z ∈ physicalPassageRegion P K C ε η)
    (hp : longitudinalCoordinate P K 0 z = 1) :
    ‖z - P 1‖ < η / 4 := by
…

Mentions: OAI.SLEExactGauge.RibbonCoordinates.physicalPassageRegion, OAI.SLEExactGauge.RibbonCoordinates.longitudinalCoordinate

theorem OAI.SLEExactGauge.RibbonCoordinates.limiting_guide_passage_neighborhood line 82

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
    (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) (hPH : MapsTo P (interior K) upperHalfPlane)
    (α : ℝ → ℂ) (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.upperHalfPlane, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate

theorem OAI.SLEExactGauge.RibbonCoordinates.eventual_early_coordinate_ball line 147

Source documentation

Local coordinate convergence and convergence of the starting tips supply the fixed early ball used by localization.

theorem eventual_early_coordinate_ball
    (pₙ : ℕ → ℂ → ℝ) (p : ℂ → ℝ) (U : Set ℂ) (hU : IsOpen U)
    (hp : ContinuousOn p U) (hconv : TendstoLocallyUniformlyOn pₙ p atTop U)
    (aₙ : ℕ → ℂ) (a : ℂ) (ha : a ∈ U) (hpa : p a = 0)
    (halim : Tendsto aₙ atTop (𝓝 a)) :
    ∃ r : ℝ, 0 < r ∧ ball a (r / 2) ⊆ U ∧
      (∀ z ∈ ball a (r / 4), p z < 1 / 3) ∧
      ∀ᶠ n in atTop, ball (aₙ n) r ⊆ U ∩ {z | pₙ n z < 1} := by
…