RibbonPassageNeighborhood.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Common physical neighborhoods of compact passage routes. Strict coordinate margins are retained on the closure before passing to moving ribbon charts.

theorem OAI.SLEExactGauge.RibbonCoordinates.isOpen_image_coordinate_subset line 17
Source documentation
An embedded coordinate chart maps every open coordinate subset of its controlled patch to an open physical subset.
```
theorem isOpen_image_coordinate_subset
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (K V : Set ℂ) (hP : ContinuousOn P K) (hi : InjOn P K)
    (hV : IsOpen V) (hVK : V ⊆ K) : IsOpen (P '' V) := by
…
```
Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness

theorem OAI.SLEExactGauge.RibbonCoordinates.common_coordinate_region_neighborhood line 33

Source documentation

A compact route strictly inside a coordinate region admits one open physical neighborhood whose closure lies in the same region for every sufficiently late ribbon chart.

theorem common_coordinate_region_neighborhood
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K A V : Set ℂ) (L : ℝ≥0)
    (hL : 0 < L) (hP : ContinuousOn P K)
    (hPn : ∀ n, ContinuousOn (Pₙ n) 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))
    (hA : IsCompact A) (hV : IsOpen V)
    (hAV : A ⊆ P '' (interior K ∩ V)) :
    ∃ U : Set ℂ, IsOpen U ∧ A ⊆ U ∧ IsCompact (closure U) ∧
      closure U ⊆ P '' (interior K ∩ V) ∧
      (∀ᶠ n in atTop, closure U ⊆ Pₙ n '' (K ∩ V)) ∧
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness

theorem OAI.SLEExactGauge.RibbonCoordinates.limit_guide_coordinates line 77

Source documentation

Limiting coordinate guides have exact longitudinal progress and retain the source transverse margin.

theorem limit_guide_coordinates
    (P : ℂ → ℂ) (K : Set ℂ) (hi : InjOn P K)
    (α : ℝ → ℂ) (x : ℝ)
    (hshape : EqOn α (fun t => P (guideCoordinate 0 x t)) (Icc 0 2))
    (hmem : ∀ t ∈ Icc (0 : ℝ) 2, guideCoordinate 0 x t ∈ K) :
    ∀ t ∈ Icc (0 : ℝ) 2,
      longitudinalCoordinate P K 0 (α t) = t ∧
        |(coordinateInverse P K (α t)).im| ≤ |x| := by
…

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