RibbonCoordinateLimit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Strict half-plane location and actual moving ribbon regions for the compact coordinate limits. The middle region has the manuscript's fixed longitudinal interval (1/3,2/3) and transverse width.

theorem OAI.SLEExactGauge.RibbonCoordinates.open_nonnegative_height_subset_upperHalfPlane line 17
Source documentation
An open planar set in the closed upper half-plane cannot meet its boundary line.
```
theorem open_nonnegative_height_subset_upperHalfPlane
    (U : Set ℂ) (hU : IsOpen U) (hheight : ∀ z ∈ U, 0 ≤ z.im) :
    U ⊆ upperHalfPlane := by
…
```
Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.RibbonCoordinates.uniform_limit_interior_upperHalfPlane line 37

Source documentation

Uniform limits of admissible embedded ribbon patches still have strictly positive height at every interior coordinate point.

theorem uniform_limit_interior_upperHalfPlane
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K : Set ℂ)
    (hP : ContinuousOn P K) (hi : InjOn P K)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hheight : ∀ n z, z ∈ K → 0 ≤ (Pₙ n z).im) :
    MapsTo P (interior K) upperHalfPlane := by
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.RibbonCoordinates.exists_bilip_halfPlane_subsequence line 56

Source documentation

The compactness output needed for a local ribbon patch includes strict limiting height, without a separate positivity assumption.

theorem exists_bilip_halfPlane_subsequence
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (K : Set ℂ) (hK : IsCompact K)
    (x₀ : ℂ) (hx₀ : x₀ ∈ K) (C L : ℝ≥0) (R : ℝ)
    (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))
    (htip : ∀ n, ‖Pₙ n x₀‖ ≤ R)
    (hheight : ∀ n z, z ∈ K → 0 ≤ (Pₙ n z).im) :
    ∃ P : ℂ → ℂ, ∃ φ : ℕ → ℕ, StrictMono φ ∧
      TendstoUniformlyOn (fun n => Pₙ (φ n)) P atTop K ∧
      LipschitzOnWith C P K ∧
      (∀ x ∈ K, ∀ y ∈ K, dist x y ≤ L * dist (P x) (P y)) ∧
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness

def OAI.SLEExactGauge.RibbonCoordinates.physicalMiddleRegion line 76
Source documentation
The actual physical middle strip in the source's local coordinates.
```
def physicalMiddleRegion (P : ℂ → ℂ) (K : Set ℂ) (k ε : ℝ) : Set ℂ :=
…
```

theorem OAI.SLEExactGauge.RibbonCoordinates.eventual_middle_region_inclusion line 81

Source documentation

Strict transverse margin on a compact common physical patch implies that its moving longitudinal band is in the actual moving middle strip.

theorem eventual_middle_region_inclusion
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K U : Set ℂ) (L : ℝ≥0) (k ε : ℝ)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (hU : IsCompact (closure U)) (hUP : closure U ⊆ P '' K)
    (hcover : ∀ᶠ n in atTop, closure U ⊆ Pₙ n '' K)
    (hwidth : ∀ z ∈ closure U, |(coordinateInverse P K z).im| < ε) :
    ∀ᶠ n in atTop,
      U ∩ {z | (1 / 3 : ℝ) < longitudinalCoordinate (Pₙ n) K k z ∧
        longitudinalCoordinate (Pₙ n) K k z < 2 / 3} ⊆
      physicalMiddleRegion (Pₙ n) K k ε := by
…

Mentions: OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse, OAI.SLEExactGauge.RibbonCoordinates.longitudinalCoordinate, OAI.SLEExactGauge.RibbonCoordinates.physicalMiddleRegion

theorem OAI.SLEExactGauge.RibbonCoordinates.source_terminal_offset line 109

Source documentation

Physical terminal control with the inverse patch constant gives the source's transverse coordinate bound at the attained front.

theorem source_terminal_offset
    (P : ℂ → ℂ) (K : Set ℂ) (L : ℝ≥0) (k ε : ℝ) (z : ℂ)
    (hL : 0 < L)
    (hlower : ∀ x ∈ K, ∀ y ∈ K, dist x y ≤ L * dist (P x) (P y))
    (hbase : ((k + 1 : ℝ) : ℂ) ∈ K) (hz : z ∈ P '' K)
    (hp : longitudinalCoordinate P K k z = 1)
    (hd : dist z (P ((k + 1 : ℝ) : ℂ)) < ε / (4 * (L : ℝ))) :
    (coordinateInverse P K z).re = k + 1 ∧
      |(coordinateInverse P K z).im| < ε / 4 := by
…

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