MergeDisks.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Merging finite physical disk families away from an obstacle

Section 2, Step 3 of the Koebe manuscript merges overlapping preliminary disks without introducing intersections of new boundaries with the lower grid obstacle. A regular cutoff gives the same merge directly: if Q is their compact union and its boundary misses F, then Q is relatively clopen in F ∪ Q. The established contour construction applied to that larger obstacle covers all of Q by disjoint smooth Jordan disks. No transversality or general-position input is required.

theorem OAI.CircleDomainRigidity.isClosed_diff_of_frontier_disjoint line 24
Source documentation
A compact region whose frontier misses a closed obstacle is relatively clopen after it is adjoined to that obstacle.
Distinct definitions of this name: OAI/Analysis/CircleDomains/Modulus/WeightedAnnularCollars.lean:16 (different declaration text). Qualify references as OAI.CircleDomainRigidity.isClosed_diff_of_frontier_disjoint@path.
```
theorem isClosed_diff_of_frontier_disjoint
    {Q F : Set ℂ} (hQ : IsClosed Q) (hF : IsClosed F)
    (hboundary : Disjoint (frontier Q) F) : IsClosed (F \ Q) := by
…
```

theorem OAI.CircleDomainRigidity.exists_smooth_jordan_cover_of_frontier_avoidance line 41

Source documentation

Smooth and fill a compact region while keeping every new boundary away from a closed obstacle. Disjointness is for the full closed fills.

theorem exists_smooth_jordan_cover_of_frontier_avoidance
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {Q F V : Set ℂ} (hQ : IsCompact Q) (hF : IsClosed F)
    (hboundary : Disjoint (frontier Q) F)
    (hV : IsOpen V) (hQV : Q ⊆ 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 ∧ (Q ⊆ ⋃ i ∈ s, jordanInterior (H i)) ∧
      s.Pairwise (fun i j => Disjoint (closure (jordanInterior (H i)))
…

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

theorem OAI.CircleDomainRigidity.exists_merged_smooth_jordan_disks line 72

Source documentation

Merge any finite family of closed Jordan disks, including overlapping ones, into disjoint smooth closed fills in the same container. It suffices that the original boundary curves miss the obstacle.

theorem exists_merged_smooth_jordan_disks
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {I : Type*} [Finite I] (D : I → ℂ ≃ₜ ℂ)
    {F V : Set ℂ} (hF : IsClosed F)
    (havoid : ∀ i, Disjoint (frontier (jordanInterior (D i))) F)
    (hV : IsOpen V) (hDV : ∀ i, closure (jordanInterior (D i)) ⊆ 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 ∧ (⋃ i, closure (jordanInterior (D i))) ⊆ (⋃ i ∈ s, jordanInterior (H i)) ∧
…

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