PhysicalTerminals.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Physical terminal disks and their staircase oscillations

A finite set of quotient dust points is surrounded by disjoint smooth physical Jordan disks, with whole fibers inside the disks and boundaries in the physical domain. The disks can be confined to prescribed neighborhoods. Liminf and limsup bounds on those neighborhoods give the staircase oscillation bound a + 4h, uniformly in width and shift.

structure OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks line 25
Source documentation
Actual terminal disks, including their smooth boundary parametrizations. The specified neighborhoods are in the quotient sphere.
```
structure PhysicalTerminalDisks {I : Type*} (G : Set Sphere) (π : Sphere → Sphere)
    (B : Set Sphere) (p : I → Sphere) (O : I → Set Sphere) where
…
```
Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_physical_terminal_disks_in_disjoint_containers line 42

Source documentation

Contours chosen in disjoint connected-complement containers have disjoint physical closures. Total disconnectedness supplies the singleton component hypothesis of the single-disk construction.

theorem exists_physical_terminal_disks_in_disjoint_containers
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {I : Type*} (G : Set Sphere) (π : Sphere → Sphere)
    (hπ : Continuous π) (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {B : Set Sphere} (hB : IsClosed B) (hTD : IsTotallyDisconnected B)
    (hbad : ∀ x ∈ Gᶜ, π x ∈ B)
    (p : I → Sphere) (hpB : ∀ i, p i ∈ B) (V : I → Set Sphere)
    (hV : ∀ i, IsOpen (V i)) (hpV : ∀ i, p i ∈ V i)
    (hVconn : ∀ i, IsConnected (V i)ᶜ)
    (hinfty : ∀ i, π OnePoint.infty ∉ closure (V i))
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_disjoint_physical_terminal_disks line 75

Source documentation

Finite prescribed neighborhoods can be replaced by disjoint smaller connected-complement containers. The exclusion of the infinity fiber is necessary for bounded physical terminal disks.

theorem exists_disjoint_physical_terminal_disks
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {I : Type*} [Fintype I] (G : Set Sphere) (π : Sphere → Sphere)
    (hπ : Continuous π) (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {B : Set Sphere} (hB : IsClosed B) (hTD : IsTotallyDisconnected B)
    (hbad : ∀ x ∈ Gᶜ, π x ∈ B)
    (p : I → Sphere) (hp : Injective p) (hpB : ∀ i, p i ∈ B)
    (hinfty : ∀ i, p i ≠ π OnePoint.infty)
    (O : I → Set Sphere) (hO : ∀ i, O i ∈ 𝓝 (p i)) :
    Nonempty (PhysicalTerminalDisks G π B p O) := by
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_physical_terminals_with_uniform_staircase_oscillation line 124

Source documentation

Actual smooth terminal boundaries obey the enlarged-band staircase estimate, for all active coordinates simultaneously and for every width and shift. hphysical records that physical points in the prescribed neighborhood are in the chosen real-branch domain. The neighborhoods may therefore also impose all desired singularity exclusions.

theorem exists_physical_terminals_with_uniform_staircase_oscillation
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {I J : Type*} [Fintype I] [Fintype J]
    (G : Set Sphere) (π : Sphere → Sphere)
    (hπ : Continuous π) (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {B : Set Sphere} (hB : IsClosed B) (hTD : IsTotallyDisconnected B)
    (hbad : ∀ x ∈ Gᶜ, π x ∈ B)
    (p : I → Sphere) (hp : Injective p) (hpB : ∀ i, p i ∈ B)
    (hinfty : ∀ i, p i ≠ π OnePoint.infty)
    (O : I → Set Sphere) (hO : ∀ i, O i ∈ 𝓝 (p i))
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere