CompactComponentContours.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Isolating a compact family of singleton components

A compact target consisting of singleton obstacle components has one compact relatively clopen obstacle neighborhood inside any prescribed open set. This strengthens pointwise isolation to the compact targets used at each stage of the descending grid construction.

theorem OAI.CircleDomainRigidity.exists_compact_piece_cover_of_singleton_components line 19

theorem OAI.CircleDomainRigidity.exists_physical_contours_for_compact_singleton_target line 57

Source documentation

Compact-target version of the physical contour construction. This is used inside one preliminary disk at a fixed label stage.

theorem exists_physical_contours_for_compact_singleton_target
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    (π : Sphere → X) (hπ : Continuous π) {F T V : Set X}
    (hF : IsClosed F) (hT : IsCompact T) (hTF : T ⊆ F)
    (hcomponents : ∀ x ∈ T, connectedComponentIn F x = {x})
    (hV : IsOpen V) (hTV : T ⊆ 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