The boundary correspondence of a conformal map

A conformal map — a holomorphic injection f on an open set U ⊆ ℂ — is a proper map onto its image: the preimage of a compact subset of f '' U is a compact subset of U. Properness is the mechanism that forces the boundary to go to the boundary, and it is the first step of the Carathéodory boundary correspondence, layer L5 of the conformal-mapping roadmap. This file proves it, deduces that a point approached from inside U is carried out of every compact subset of f '' U, and packages the consequences for a map that does extend continuously to closure U: such an extension carries frontier U into frontier (f '' U), onto it once U is in addition bounded, and — when the extension is injective on closure U — is a homeomorphism of the closures.

The existence of the continuous extension is the hard, hypothesis-laden half of Carathéodory's theorem (it needs the boundary of the image to be a Jordan curve, or at least locally connected), and it is not proved here; the L5 milestone is that existence statement. What is proved here is everything that holds unconditionally, plus the packaging that turns the extension, once it is available, into the boundary homeomorphism the milestone asks for.

The argument

Properness is the inverse function theorem in disguise. An injective holomorphic map on an open set is an open partial homeomorphism onto its image (DifferentiableOn.toOpenPartialHomeomorph), and U ∩ f ⁻¹' K is exactly the image of K under its inverse Function.invFunOn f U, so it is compact as the continuous image of a compact set. Everything else follows from that one fact. If z i → w with z i ∈ U and w ∉ U, then f (z i) cannot lie in a compact K ⊆ f '' U frequently: otherwise z i would frequently lie in the compact — hence closed — set U ∩ f ⁻¹' K, which would then contain the limit w.

For a boundary point w ∈ frontier U, the filter 𝓝[U] w is the one to run this along: it is NeBot precisely because w ∈ closure U. If a continuous extension F had F w inside the open set f '' U, then a small closed ball around F w would be a compact subset of f '' U that f = F enters eventually along 𝓝[U] w by continuity, and leaves eventually by properness — impossible on a nontrivial filter. Hence F w ∉ f '' U, while F w ∈ closure (f '' U) because F is continuous on closure U; that is membership in frontier (f '' U).

The argument beyond the two holomorphic inputs — the open mapping theorem, through TauCeti.isOpen_image_of_differentiableOn_of_injOn, and its packaging as an open partial homeomorphism — is purely topological, and no continuity hypothesis on the inverse of f appears precisely because those two supply it. In accordance with the generality bar of ConformalMapping/README.md, which fixes scalar ℂ for every theorem added in layers L0–L6, the results are stated for conformal maps of ℂ rather than for an abstract proper map.

Main results

• TauCeti.isCompact_inter_preimage_of_differentiableOn_of_injOn — a conformal map is proper onto its image: U ∩ f ⁻¹' K is compact for compact K ⊆ f '' U.
• TauCeti.eventually_notMem_of_tendsto_of_notMem — a family in U converging to a point outside U, in particular to a boundary point, is carried out of every compact subset of the image.
• TauCeti.notMem_image_of_mem_frontier — a continuous extension to closure U sends frontier U outside f '' U.
• TauCeti.image_closure_eq_closure_image — for bounded U, a continuous extension carries closure U onto closure (f '' U).
• TauCeti.image_frontier_subset_frontier_image — a continuous extension carries frontier U into frontier (f '' U); no boundedness is needed.
• TauCeti.image_frontier_eq_frontier_image — for bounded U, that inclusion is an equality: a continuous extension carries frontier U onto frontier (f '' U).
• TauCeti.bijOn_closure_closure_image and TauCeti.closureHomeomorph — for bounded U, an extension injective on closure U is a homeomorphism closure U ≃ₜ closure (f '' U).

Coordination with upstream Mathlib

Mathlib has no boundary correspondence for conformal maps, and — unlike the L0–L3 material — layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, which stops at the mapping theorem itself. So this file is new Lean formalization rather than a temporary shim. It does consume the L0–L3 shims TauCeti.isOpen_image_of_differentiableOn_of_injOn and DifferentiableOn.toOpenPartialHomeomorph, which are to be refactored onto Mathlib once the upstream work lands.

References

• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IX.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.

Properness

theorem TauCeti.isCompact_inter_preimage_of_differentiableOn_of_injOn {U K : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hfd : DifferentiableOn ℂ f U) (hfi : Set.InjOn f U) (hK : IsCompact K) (hKf : K ⊆ f '' U) : IsCompact (U ∩ f ⁻¹' K)

A conformal map is proper onto its image. If f is holomorphic and injective on an open set U and K ⊆ f '' U is compact, then the part of the preimage of K lying in U is compact.

Properness is what distinguishes f '' U as the whole image: the preimage cannot escape to the boundary of U while its image stays in a compact part of f '' U.

theorem TauCeti.eventually_notMem_of_tendsto_of_notMem {U K : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} {l : Filter ι} {z : ι → ℂ} {w : ℂ} (hUo : IsOpen U) (hfd : DifferentiableOn ℂ f U) (hfi : Set.InjOn f U) (hz : ∀ᶠ (i : ι) in l, z i ∈ U) (hlim : Filter.Tendsto z l (nhds w)) (hwU : w ∉ U) (hK : IsCompact K) (hKf : K ⊆ f '' U) : ∀ᶠ (i : ι) in l, f (z i) ∉ K

A conformal map carries a family converging out of U out of every compact subset of the image. If z i ∈ U eventually, z i → w and w ∉ U, then eventually f (z i) avoids any compact K ⊆ f '' U.

Continuous extensions to the closure

theorem TauCeti.notMem_image_of_mem_frontier {U : Set ℂ} {f F : ℂ → ℂ} (hUo : IsOpen U) (hfd : DifferentiableOn ℂ f U) (hfi : Set.InjOn f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) {w : ℂ} (hw : w ∈ frontier U) : F w ∉ f '' U

A continuous extension of a conformal map sends the boundary off the image. If F is continuous on closure U and agrees with f on U, then F maps no boundary point of U into the open set f '' U.

For open U the hypothesis w ∈ frontier U is w ∈ closure U together with w ∉ U; both halves are used, the first to make the filter 𝓝[U] w nontrivial and the second to invoke TauCeti.eventually_notMem_of_tendsto_of_notMem.

theorem TauCeti.image_closure_eq_closure_image {U : Set ℂ} {f F : ℂ → ℂ} (hUb : Bornology.IsBounded U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) : F '' closure U = closure (f '' U)

A continuous extension of a conformal map carries the closure onto the closure of the image, for a bounded U. Only boundedness and continuity are used; no holomorphy hypothesis appears.

theorem TauCeti.image_frontier_subset_frontier_image {U : Set ℂ} {f F : ℂ → ℂ} (hUo : IsOpen U) (hfd : DifferentiableOn ℂ f U) (hfi : Set.InjOn f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) : F '' frontier U ⊆ frontier (f '' U)

A continuous extension of a conformal map carries the boundary into the boundary. No boundedness is needed.

theorem TauCeti.image_frontier_eq_frontier_image {U : Set ℂ} {f F : ℂ → ℂ} (hUo : IsOpen U) (hUb : Bornology.IsBounded U) (hfd : DifferentiableOn ℂ f U) (hfi : Set.InjOn f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) : F '' frontier U = frontier (f '' U)

A continuous extension of a conformal map carries the boundary onto the boundary, for a bounded U. No injectivity of the extension is needed, only the injectivity of f on U that makes it conformal: the inclusion of TauCeti.image_frontier_subset_frontier_image is an equality because a point of frontier (f '' U) lies in closure (f '' U) = F '' closure U, so it is F z for some z ∈ closure U, and z ∈ U is impossible — it would put F z = f z back inside the open set f '' U, which frontier (f '' U) avoids.

The boundary homeomorphism

theorem TauCeti.bijOn_closure_closure_image {U : Set ℂ} {f F : ℂ → ℂ} (hUb : Bornology.IsBounded U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hFi : Set.InjOn F (closure U)) : Set.BijOn F (closure U) (closure (f '' U))

An injective continuous extension is a bijection of the closures. If F is continuous on closure U for a bounded U, agrees with f on U, and is injective on closure U, then it maps closure U bijectively onto closure (f '' U). The set-level form of TauCeti.closureHomeomorph: injectivity is the hypothesis, and surjectivity onto closure (f '' U) is TauCeti.image_closure_eq_closure_image. Neither holomorphy of f nor openness of U is needed; a conformal f is the intended application.

noncomputable def TauCeti.closureHomeomorph {U : Set ℂ} {f F : ℂ → ℂ} (hUb : Bornology.IsBounded U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hFi : Set.InjOn F (closure U)) : ↑(closure U) ≃ₜ ↑(closure (f '' U))

The homeomorphism of closures induced by an injective continuous extension. If F is continuous on closure U for a bounded U, agrees with f on U, and is injective on closure U, then F is a homeomorphism of closure U onto closure (f '' U). Neither holomorphy of f nor openness of U is assumed; the intended instance is a conformal map f on an open U together with a continuous extension F.

For a Riemann map of a Jordan domain this is the conclusion the Carathéodory correspondence (layer L5) asks for; what that milestone adds is the existence of such an F, which is not proved here. Continuity of the inverse is free: closure U is compact and ℂ is Hausdorff.

The definition is not exposed; TauCeti.coe_closureHomeomorph_apply and TauCeti.coe_closureHomeomorph_symm_apply are its characterizations.

Equations

• TauCeti.closureHomeomorph hUb hFc hFf hFi = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem TauCeti.coe_closureHomeomorph_apply {U : Set ℂ} {f F : ℂ → ℂ} (hUb : Bornology.IsBounded U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hFi : Set.InjOn F (closure U)) (x : ↑(closure U)) : ↑((closureHomeomorph hUb hFc hFf hFi) x) = F ↑x

The boundary homeomorphism is the extension F itself.

@[simp]

theorem TauCeti.coe_closureHomeomorph_symm_apply {U : Set ℂ} {f F : ℂ → ℂ} (hUb : Bornology.IsBounded U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hFi : Set.InjOn F (closure U)) (y : ↑(closure (f '' U))) : ↑((closureHomeomorph hUb hFc hFf hFi).symm y) = Function.invFunOn F (closure U) ↑y

The inverse of the boundary homeomorphism is the set-level inverse Function.invFunOn F (closure U).