Documentation

TauCeti.Analysis.Complex.Conformal.Jordan.Domain

Jordan domains, and the domains a conformal map takes onto a disc #

A Jordan domain is a bounded domain of ℂ whose boundary is a Jordan curve. This file introduces TauCeti.IsJordanDomain, exhibits the discs as the basic example, and proves the converse half of the Carathéodory boundary correspondence: a bounded domain that a conformal map carries onto a disc, the map extending continuously and injectively to the closure, is a Jordan domain.

Why the converse is the accessible half #

Layer L5 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md) is Carathéodory's theorem: the Riemann map of a Jordan domain extends to a homeomorphism of the closures. Both directions of that correspondence pass through the same object, the boundary homeomorphism TauCeti.closureHomeomorph, but they are not of the same difficulty. Producing the extension is the hard direction — it needs the boundary geometry to control the cluster sets of the map, which is where Conformal/ClusterSet.lean and the local connectivity of the boundary enter, and it is not proved here. Reading the boundary geometry off an extension that is already given is the direction this file supplies, and it is short, because the boundary correspondence has already been established: TauCeti.image_frontier_eq_frontier_image says that an injective continuous extension carries frontier U onto frontier (f '' U), and frontier U is compact whenever U is bounded, so TauCeti.IsJordanCurve.of_image transports the circle backwards along the extension.

The result is exactly the statement that Carathéodory's hypothesis is not merely sufficient but necessary: among bounded domains, "conformally a disc, with the map extending to a homeomorphism of the closures" implies "Jordan". It is what makes the L5 milestone a correspondence rather than a one-way sufficient condition, and it is the form in which the boundary hypothesis is checked in practice, since a Riemann map is rarely available in closed form while its boundary values often are.

Main definitions #

Main results #

Generality #

In accordance with the generality bar of ConformalMapping/README.md, which fixes scalar ℂ for every theorem added in layers L0–L6, the results below are stated for maps of ℂ, as in Conformal/BoundaryCorrespondence.lean; the Jordan-curve vocabulary they are phrased in, together with the circle that models it, is in TauCeti/Topology/JordanCurve/Basic.lean, where the predicate and its transfer lemmas are stated for an arbitrary topological space.

Coordination with upstream Mathlib #

Layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, which stops at the mapping theorem itself, and the pinned Mathlib has no Jordan-curve vocabulary at all. So this file is new Lean formalization rather than a temporary shim. It consumes, through Conformal/BoundaryCorrespondence.lean, the L0–L3 shim TauCeti.isOpen_image_of_differentiableOn_of_injOn, to be refactored onto Mathlib once the upstream work lands.

References #

Jordan domains, and the convex domains among them #

source
structure TauCeti.IsJordanDomain (U : Set ℂ) :
Prop

A Jordan domain: a bounded domain of ℂ bounded by a Jordan curve.

Boundedness is part of the definition: the two complementary domains of a Jordan curve in the sphere have the same boundary, and it is the bounded one — the interior of the curve — that the Carathéodory correspondence compares to the unit disc.

Instances For
    source
    theorem TauCeti.isJordanDomain_of_convex {U : Set ℂ} (hU : Convex ℝ U) (ho : IsOpen U) (hne : U.Nonempty) (hb : Bornology.IsBounded U) :
    IsJordanDomain U

    A bounded convex domain of ℂ is a Jordan domain.

    This is TauCeti.isJordanDomain_ball with the disc weakened to an arbitrary convex domain, which it recovers at U = Metric.ball c r. An elliptical disc, the interior of a convex polygon, and any nonempty bounded intersection of finitely many open half-planes are Jordan domains — finitely many, since an infinite intersection of open half-planes is convex but need not be open.

    Of the four defining conditions, openness and boundedness are the hypotheses ho and hb, taken over unchanged. Connectedness is hU with hne: a nonempty convex set is connected. The Jordan frontier is hU, hne and hb together, by TauCeti.isJordanCurve_frontier_of_convex, whose solidity hypothesis (interior U).Nonempty is hne read through ho, the interior of an open set being the set itself.

    source
    theorem TauCeti.isJordanDomain_ball {r : ℝ} (c : ℂ) (hr : 0 < r) :
    IsJordanDomain (Metric.ball c r)

    A disc of positive radius is a Jordan domain: it is a bounded convex domain, and its frontier is the circle of the same centre and radius. This is the model Jordan domain, and the target of every Riemann map.

    source
    theorem TauCeti.IsJordanCurve.isJordanDomain_filledHull_sdiff_of_locally_eq_line {r : ℝ} {C : Set ℂ} (hC : IsJordanCurve C) {p v : ℂ} (hr : 0 < r) (hline : ∀ z ∈ Metric.ball p r, z ∈ C ↔ (v * (z - p)).im = 0) :
    IsJordanDomain (filledHull C \ C)

    The inside of a Jordan curve with a straight piece is a Jordan domain. If a Jordan curve C agrees with a line in a ball about one of its points — as a polygon does at an interior point of one of its sides — then its filled hull minus C, the bounded complementary component, is a Jordan domain with frontier C.

    Elementary consequences of being a Jordan domain #

    source
    theorem TauCeti.IsJordanDomain.nonempty {U : Set ℂ} (h : IsJordanDomain U) :
    U.Nonempty

    A Jordan domain is nonempty.

    source
    theorem TauCeti.IsJordanDomain.isCompact_closure {U : Set ℂ} (h : IsJordanDomain U) :
    IsCompact (closure U)

    The closure of a Jordan domain is compact.

    source
    theorem TauCeti.IsJordanDomain.frontier_nonempty {U : Set ℂ} (h : IsJordanDomain U) :
    (frontier U).Nonempty

    The frontier of a Jordan domain is nonempty; in particular a Jordan domain is a proper open subset of ℂ, so that, being also simply connected (TauCeti.IsJordanDomain.isSimplyConnected), it satisfies the hypotheses of the Riemann mapping theorem.

    source
    theorem TauCeti.IsJordanDomain.locallyConnectedSpace_frontier {U : Set ℂ} (h : IsJordanDomain U) :
    LocallyConnectedSpace ↑(frontier U)

    The boundary of a Jordan domain is locally connected, being a Jordan curve (TauCeti.IsJordanCurve.locallyConnectedSpace).

    This is the hypothesis under which Carathéodory's continuity theorem produces the continuous extension, so it is what the hard direction of the L5 milestone asks of a Jordan domain; the converse reading — that any continuous extension carries local connectedness to the image boundary — is TauCeti.locallyConnectedSpace_frontier_image in Conformal/LocallyConnectedBoundary.lean.

    source
    theorem TauCeti.IsJordanDomain.isUniformlyLocallyConnected_frontier {U : Set ℂ} (h : IsJordanDomain U) :
    IsUniformlyLocallyConnected (frontier U)

    The boundary of a Jordan domain is uniformly locally connected: nearby boundary points are joined by connected subsets of the boundary that are small at a rate independent of where they sit.

    This is TauCeti.IsJordanDomain.locallyConnectedSpace_frontier upgraded by IsCompact.isUniformlyLocallyConnected, costing nothing because the boundary of a bounded set is compact. The uniform form is what the hard direction of the L5 milestone consumes: Carathéodory's continuity theorem controls the image of a crosscut by joining its two boundary endpoints inside a small connected piece of frontier U, and the estimate has to be uniform over all crosscuts at once.

    source
    theorem TauCeti.IsJordanDomain.ne_univ {U : Set ℂ} (h : IsJordanDomain U) :
    U ≠ Set.univ

    A Jordan domain is not all of ℂ.

    source
    theorem TauCeti.IsJordanDomain.isSimplyConnected {U : Set ℂ} (h : IsJordanDomain U) :
    IsSimplyConnected U

    A Jordan domain is simply connected. Its frontier is a Jordan curve, hence connected, and its complement is unbounded because the domain is bounded, so it has no holes (TauCeti.isSimplyConnected_of_isPreconnected_frontier). Together with TauCeti.IsJordanDomain.ne_univ, this says that a Jordan domain satisfies the hypotheses of the Riemann mapping theorem.

    The converse half of the Carathéodory correspondence #

    source
    theorem TauCeti.isJordanCurve_frontier_of_isJordanCurve_frontier_image {U : Set ℂ} {f F : ℂ → ℂ} (hUo : IsOpen U) (hUb : Bornology.IsBounded U) (hfd : DifferentiableOn ℂ f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hFi : Set.InjOn F (closure U)) (h : IsJordanCurve (frontier (f '' U))) :
    IsJordanCurve (frontier U)

    A conformal map with an injective continuous extension transports the Jordan property back across the boundary. If a holomorphic f on a bounded open U has a continuous extension F to closure U that is injective there, and the frontier of the image f '' U is a Jordan curve, then so is the frontier of U.

    The extension carries frontier U onto frontier (f '' U) (TauCeti.image_frontier_eq_frontier_image) and is continuous and injective there, and frontier U is compact because U is bounded; TauCeti.IsJordanCurve.of_image does the rest. Injectivity of f on U is not assumed: it follows from that of F on closure U.

    source
    theorem TauCeti.isJordanDomain_of_isJordanCurve_frontier_image {U : Set ℂ} {f F : ℂ → ℂ} (hUo : IsOpen U) (hUb : Bornology.IsBounded U) (hfd : DifferentiableOn ℂ f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hFi : Set.InjOn F (closure U)) (himgc : IsConnected (f '' U)) (himg : IsJordanCurve (frontier (f '' U))) :
    IsJordanDomain U

    The converse half of the Carathéodory boundary correspondence. A bounded open set of ℂ that a holomorphic map carries onto a connected set with Jordan frontier, extending continuously and injectively to the closure, is itself a Jordan domain.

    Carathéodory's theorem — layer L5 of the conformal-mapping roadmap — is the converse for the disc: for a Jordan domain such an extension exists. Together the two say that, among bounded domains, being a Jordan domain is exactly the condition under which the Riemann map extends to a homeomorphism of the closures.

    Only two of the four properties of a Jordan domain are asked of the image, since the other two are already carried across by f: the image of an open set under an injective holomorphic map is open, and the image is bounded because F is continuous on the compact closure U. A caller holding h : TauCeti.IsJordanDomain (f '' U) supplies h.isConnected and h.isJordanCurve_frontier. Connectedness of U itself is likewise not assumed: f is an open partial homeomorphism of U onto f '' U (DifferentiableOn.toOpenPartialHomeomorph), so U is the image of the connected f '' U under the continuous inverse.

    source
    theorem TauCeti.isJordanDomain_of_image_eq_ball {U : Set ℂ} {f F : ℂ → ℂ} {c : ℂ} {r : ℝ} (hUo : IsOpen U) (hUb : Bornology.IsBounded U) (hfd : DifferentiableOn ℂ f U) (hFc : ContinuousOn F (closure U)) (hFf : Set.EqOn F f U) (hFi : Set.InjOn F (closure U)) (hr : 0 < r) (himg : f '' U = Metric.ball c r) :
    IsJordanDomain U

    The converse half of the Carathéodory boundary correspondence, for the disc. A bounded open set of ℂ that a holomorphic map carries onto a disc, extending continuously and injectively to the closure, is a Jordan domain.

    This is the case of TauCeti.isJordanDomain_of_isJordanCurve_frontier_image in which the image is the model Jordan domain, and it is the form the Carathéodory correspondence is stated in, the disc being the target of every Riemann map.