SmoothJordanNeighborhoods.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite smooth Jordan neighborhoods

The contour construction in Section 1 of the Koebe manuscript is derived from the smooth cutoff and regular level, scalar Sard, compact one-manifold classification, and planar Schoenflies. Outer selection and containment give the finite family of Jordan neighborhoods.

theorem OAI.CircleDomainRigidity.frontier_superlevel_eq_regular_level line 22
Source documentation
Every point of a regular level borders its strict superlevel set. Otherwise the point is a local maximum, contradicting regularity.
```
theorem frontier_superlevel_eq_regular_level {f : ℂ → ℝ} {t : ℝ}
    (hf : Continuous f) (ht : IsPlanarRegularValue f t) :
    frontier {z | t < f z} = {z | f z = t} := by
…
```
Mentions: OAI.CircleDomainRigidity.IsPlanarRegularValue
theorem OAI.CircleDomainRigidity.closed_jordanInterior_subset_of_unbounded_connected_compl line 45
Source documentation
A connected unbounded exterior cannot enter the bounded side of a Jordan curve that it misses. This applies to physical inverse images of quotient Jordan neighborhoods, even when their boundaries are not smooth.
```
theorem closed_jordanInterior_subset_of_unbounded_connected_compl
    (H : ℂ ≃ₜ ℂ) {V : Set ℂ}
    (hV : IsPreconnected Vᶜ) (hVunbounded : ¬ Bornology.IsBounded Vᶜ)
    (hfront : frontier (jordanInterior H) ⊆ V) :
    closure (jordanInterior H) ⊆ V := by
…
```
Mentions: OAI.CircleDomainRigidity.jordanInterior

theorem OAI.CircleDomainRigidity.exists_finite_smooth_jordan_cover line 71

Source documentation

Actual finite smooth Jordan disks covering a chosen compact part of an obstacle, with disjoint closures contained in the prescribed physical open set. Its complement is required connected and unbounded precisely for the hole-filling containment argument.

theorem exists_finite_smooth_jordan_cover
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {A F V : Set ℂ} (hA : IsCompact A) (hAF : A ⊆ F)
    (hFA : IsClosed (F \ A)) (hV : IsOpen V) (hAV : A ⊆ V)
    (hVconn : IsPreconnected Vᶜ) (hVunbounded : ¬ Bornology.IsBounded Vᶜ) :
    ∃ (f : ℂ → ℝ) (t : ℝ)
      (γ : ConnectedComponents {z // f z = t} → Circle → ℂ)
      (H : ConnectedComponents {z // f z = t} → ℂ ≃ₜ ℂ)
      (s : Set (ConnectedComponents {z // f z = t})),
      s.Finite ∧ A ⊆ ⋃ i ∈ s, jordanInterior (H i) ∧
      s.Pairwise (fun i j => Disjoint (closure (jordanInterior (H i)))
        (closure (jordanInterior (H j)))) ∧
…

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