One image piece of a crosscut lies inside a compact enclosing set

For a holomorphic injection of an open set U, one of the two image pieces — the near side U ∩ ball ζ ρ or the far side U \ closedBall ζ ρ — lies in the filled hull of a closed bounded set K through the image crosscut. The hypotheses are:

• K contains the image crosscut and is contained in its closure union frontier (f '' U).
• K \ {f z₀} is preconnected at a chosen crosscut point z₀.
• The two image pieces are preconnected (hAc, hBc). For U = ball c r these follow from the ball geometry (isConnected_ball_inter_ball, isConnected_ball_diff_closedBall).

The transversal segment through a point of the crosscut has the near side on one side and the far side on the other; the winding-number two-sidedness theorem (Contour.mem_filledHull_or_mem_filledHull_of_isPreconnected_sdiff_singleton) puts one end in the filled hull. No Jordan curve theorem is used.

This is the planar-separation step of the ConformalMapping roadmap (L5).

Layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, and Mathlib has no boundary correspondence for conformal maps, so this is new Lean formalization rather than a temporary shim.

Main results

• TauCeti.exists_pos_forall_mem_image_inter_ball_and_image_sdiff_closedBall — the transversal segment through a point of the image crosscut, with near side and far side on opposite sides.
• TauCeti.mem_closure_image_inter_sphere_inter_setOf_im_pos_and_mem_closure_inter_setOf_im_neg — the image crosscut is adherent to each of its points from both sides of the transversal.
• TauCeti.image_inter_ball_subset_filledHull_or_image_sdiff_closedBall_subset_filledHull — one of the two image pieces lies in the filled hull of a closed bounded set through the image crosscut. Requires K \ {f z₀} preconnected.
• TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton — diameter selection: when the enclosing set is narrower than the far side, the near side is enclosed. Consumes the disjunction above; IsJordanCurve.isPathConnected_sdiff_singleton discharges the preconnectedness hypothesis in the intended application.
• TauCeti.image_inter_ball_subset_filledHull_of_frontier_subset — the enclosure hypothesis is implied by the boundary-piece hypothesis of Conformal/CutDiameter.lean.

References

• C. Carathéodory, Über die Begrenzung einfach zusammenhängender Gebiete, Math. Ann. 73, 1913.
• P. L. Duren, Univalent Functions, Chapter 3.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Section 2.3.
• J. B. Garnett and D. E. Marshall, Harmonic Measure, Theorem I.3.1.

theorem TauCeti.exists_pos_forall_mem_image_inter_ball_and_image_sdiff_closedBall {f : ℂ → ℂ} {ζ z₀ : ℂ} {ρ : ℝ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) (hz₀ : z₀ ∈ U ∩ Metric.sphere ζ ρ) (hρ : 0 < ρ) : ∃ (η : ℝ), 0 < η ∧ (∀ t ∈ Set.Ioo (-η) 0, deriv f z₀ * (z₀ - ζ) * ↑t + f z₀ ∈ f '' (U ∩ Metric.ball ζ ρ)) ∧ ∀ t ∈ Set.Ioo 0 η, deriv f z₀ * (z₀ - ζ) * ↑t + f z₀ ∈ f '' (U \ Metric.closedBall ζ ρ)

The transversal segment through a point of the image crosscut. For small negative t the segment lies in the image of the near side, and for small positive t in the far side.

theorem TauCeti.mem_closure_image_inter_sphere_inter_setOf_im_pos_and_mem_closure_inter_setOf_im_neg {f : ℂ → ℂ} {ζ z₀ : ℂ} {ρ : ℝ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) (hz₀ : z₀ ∈ U ∩ Metric.sphere ζ ρ) (hρ : 0 < ρ) : f z₀ ∈ closure (f '' (U ∩ Metric.sphere ζ ρ) ∩ {q : ℂ | 0 < ((q - f z₀) / (deriv f z₀ * (z₀ - ζ))).im}) ∧ f z₀ ∈ closure (f '' (U ∩ Metric.sphere ζ ρ) ∩ {q : ℂ | ((q - f z₀) / (deriv f z₀ * (z₀ - ζ))).im < 0})

The image crosscut is adherent from both sides of the transversal segment. In the transversal coordinate the crosscut has velocity i at the crossing point.

theorem TauCeti.image_inter_ball_subset_filledHull_or_image_sdiff_closedBall_subset_filledHull {f : ℂ → ℂ} {ζ : ℂ} {ρ : ℝ} {U : Set ℂ} (hUo : IsOpen U) (hρ : 0 < ρ) (hf : DifferentiableOn ℂ f U) (hinj : Set.InjOn f U) (hAc : IsPreconnected (U ∩ Metric.ball ζ ρ)) (hBc : IsPreconnected (U \ Metric.closedBall ζ ρ)) {K : Set ℂ} (hK : IsClosed K) (hKb : Bornology.IsBounded K) (hγK : f '' (U ∩ Metric.sphere ζ ρ) ⊆ K) (hKsub : K ⊆ closure (f '' (U ∩ Metric.sphere ζ ρ)) ∪ frontier (f '' U)) {z₀ : ℂ} (hz₀ : z₀ ∈ U ∩ Metric.sphere ζ ρ) (hKp : IsPreconnected (K \ {f z₀})) : f '' (U ∩ Metric.ball ζ ρ) ⊆ filledHull K ∨ f '' (U \ Metric.closedBall ζ ρ) ⊆ filledHull K

One of the two image pieces lies in the filled hull of a closed bounded set through the image crosscut. The transversal segment meets the set only at the crossing point, and the set minus that point is preconnected, so the winding-number two-sidedness theorem applies. The preconnectedness hypothesis hKp is required only at the selected crossing point z₀, not at every crosscut point.

theorem TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton {f : ℂ → ℂ} {ζ : ℂ} {ρ : ℝ} {U : Set ℂ} (hUo : IsOpen U) (hρ : 0 < ρ) (hf : DifferentiableOn ℂ f U) (hinj : Set.InjOn f U) (hAc : IsPreconnected (U ∩ Metric.ball ζ ρ)) (hBc : IsPreconnected (U \ Metric.closedBall ζ ρ)) {K : Set ℂ} (hK : IsClosed K) (hKb : Bornology.IsBounded K) (hγK : f '' (U ∩ Metric.sphere ζ ρ) ⊆ K) (hKsub : K ⊆ closure (f '' (U ∩ Metric.sphere ζ ρ)) ∪ frontier (f '' U)) {z₀ : ℂ} (hz₀ : z₀ ∈ U ∩ Metric.sphere ζ ρ) (hKp : IsPreconnected (K \ {f z₀})) (hlt : Metric.diam K < Metric.diam (f '' (U \ Metric.closedBall ζ ρ))) : f '' (U ∩ Metric.ball ζ ρ) ⊆ filledHull K

Diameter selection: when the enclosing set is narrower than the far side, the near side is enclosed. This consumes the disjunction TauCeti.image_inter_ball_subset_filledHull_or_image_sdiff_closedBall_subset_filledHull by excluding the far-side case: trapping the far side inside K gives diam (f '' (U \ closedBall ζ ρ)) ≤ diam K, contradicting the hypothesis. The plane-separation input p ∈ closure (filledHull K \ K) is replaced by preconnectedness of K \ {f z₀}, which is discharged by IsJordanCurve.isPathConnected_sdiff_singleton in the intended application.

The frontier route to enclosure

theorem TauCeti.image_inter_ball_subset_filledHull_of_frontier_subset {f : ℂ → ℂ} {ζ : ℂ} {ρ : ℝ} {U : Set ℂ} (hUo : IsOpen U) (hd : DifferentiableOn ℂ f U) (hinj : Set.InjOn f U) (hb : Bornology.IsBounded (f '' (U ∩ Metric.ball ζ ρ))) {E : Set ℂ} (hE : frontier (f '' U) ∩ frontier (f '' (U ∩ Metric.ball ζ ρ)) ⊆ E) : f '' (U ∩ Metric.ball ζ ρ) ⊆ filledHull (f '' (U ∩ Metric.sphere ζ ρ) ∪ E)

A boundary piece enclosing what the near side clings to encloses the near side. If every boundary point of the image domain on the frontier of the near image side lies in E, then the frontier of that side lies in f '' (U ∩ sphere ζ ρ) ∪ E by TauCeti.frontier_image_inter_ball_subset, so TauCeti.subset_filledHull_of_frontier_subset encloses the side.

Thus the frontier route supplies the same filled-hull inclusion as the enclosure route, with the same E; either inclusion becomes a width bound on the near side by TauCeti.diam_le_diam_of_subset_filledHull.