SmallPhysicalDisks.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small physical disks at singleton quotient components

A singleton component of a closed quotient obstacle has a compact relatively clopen neighborhood inside any prescribed open neighborhood. Pulling it back and applying the proved smooth contour construction gives actual physical Jordan disks. The boundaries avoid the entire quotient obstacle, and hence lie in the physical domain whenever that obstacle contains the collapsed complementary components.

theorem OAI.CircleDomainRigidity.exists_compact_piece_of_singleton_component line 24

Source documentation

The compact relatively clopen obstacle piece used before smoothing.

theorem exists_compact_piece_of_singleton_component
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    {F V : Set X} (hF : IsClosed F) {x : X} (hx : x ∈ F)
    (hcomponent : connectedComponentIn F x = {x})
    (hV : IsOpen V) (hxV : x ∈ V) :
    ∃ A : Set X, IsCompact A ∧ x ∈ A ∧ A ⊆ F ∧ A ⊆ V ∧ IsClosed (F \ A) := by
…

theorem OAI.CircleDomainRigidity.isCompact_finite_preimage line 65
Source documentation
Closed sphere sets avoiding infinity have compact finite-coordinate preimages. This is the concrete properness needed for the obstacle piece.
```
theorem isCompact_finite_preimage {K : Set Sphere} (hK : IsClosed K) (hinfty : OnePoint.infty ∉ K) :
    IsCompact (((↑) : ℂ → Sphere) ⁻¹' K) :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.exists_small_physical_disks_at_singleton_component line 72

Source documentation

Finite smooth disk cover of the physical fiber at a singleton quotient component. The connected unbounded complement condition is imposed on the specified physical preimage, exactly where the filling argument uses it.

theorem exists_small_physical_disks_at_singleton_component
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    (π : Sphere → X) (hπ : Continuous π) {F V : Set X}
    (hF : IsClosed F) {x : X} (hx : x ∈ F)
    (hcomponent : connectedComponentIn F x = {x})
    (hV : IsOpen V) (hxV : x ∈ V) (hinfty : π OnePoint.infty ∉ V)
    (hVconn : IsPreconnected ((fun z : ℂ => π (z : Sphere)) ⁻¹' V)ᶜ)
    (hVunbounded : ¬ Bornology.IsBounded ((fun z : ℂ => π (z : Sphere)) ⁻¹' V)ᶜ)
    {G : Set Sphere} (hbad : ∀ p ∈ Gᶜ, π p ∈ F) :
    ∃ (f : ℂ → ℝ) (t : ℝ)
      (γ : ConnectedComponents {z // f z = t} → Circle → ℂ)
…

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