Continuous logarithms on a set, and the Borsuk map of two points

A complex-valued function g has a continuous logarithm on a set S when some h, continuous on S, satisfies exp (h x) = g x throughout S; this file introduces that predicate, TauCeti.HasContinuousLogOn, and proves the two elementary facts about it that planar separation arguments run on.

The predicate is the natural home of the classical nonvanishing plus no winding condition. It implies g is continuous and zero-free on S but is strictly stronger, and unlike Mathlib's Complex.exists_continuousOn_eqOn_exp_comp — which produces a logarithm on a simply connected open set — it makes sense, and is genuinely restrictive, on a set with no interior at all: a compact K ⊆ ℂ such as a curve. That is exactly the case the separation theory needs, so the existence statement has to become a predicate carrying its own algebra rather than a one-off lemma. That algebra is the one the zero-free continuous functions carry: the property is closed under multiplication and under inversion, the witnesses adding (TauCeti.HasContinuousLogOn.mul) and negating (TauCeti.HasContinuousLogOn.inv) accordingly; it restricts along inclusions, and it holds outright when g avoids the slit Complex.slitPlaneᶜ, where the principal branch works (TauCeti.hasContinuousLogOn_of_mapsTo_slitPlane).

Gluing along a connected overlap

The first substantial fact is that continuous logarithms glue: if S and T are closed, their overlap S ∩ T is preconnected, and g has a continuous logarithm on each, then it has one on S ∪ T (TauCeti.HasContinuousLogOn.union). Two logarithms of the same function differ by a value of Complex.exp ⁻¹' {1}, that is by an integer multiple of 2 * π * I; distinct such multiples are 2 * π apart, so that fibre is a discrete subset of ℂ and the difference, being continuous on a preconnected overlap, is constant there. So one logarithm can be shifted by a single constant to agree with the other on the overlap, and the two then define one continuous function on the closed union. The constancy step is isolated as TauCeti.eq_of_isPreconnected_of_forall_exp_eq_one.

The Borsuk map

For a b : ℂ the Borsuk map of the pair is z ↦ (z - a) / (z - b), defined and zero-free off {a, b}. Its logarithms detect how a set sits between the two points: the main theorem here is that if b lies in the connected component of a in the complement of a closed K, then the Borsuk map has a continuous logarithm on K (TauCeti.hasContinuousLogOn_sub_div_sub). Equivalently, in contrapositive form: if the Borsuk map admits no continuous logarithm on K, then b ∉ connectedComponentIn Kᶜ a — which, once both points are known to lie outside K, says that K separates a from b.

The proof is a connectedness argument on the second point, not a construction. Call w good if z ↦ (z - a) / (z - w) has a continuous logarithm on K. The point a is good, its Borsuk map being the constant 1. Moving w by less than half the distance from w to K multiplies the Borsuk map by z ↦ (z - w) / (z - w'), a function whose values lie within distance 1 of 1 and hence in the slit plane, so that factor has a logarithm of its own (TauCeti.hasContinuousLogOn_sub_div_sub_of_norm_lt) and goodness transfers — in both directions, since the estimate is symmetric. So the good and the bad points of Kᶜ are both open, and the component of a is preconnected, hence entirely good.

What this settles, and what it does not

Only one implication of the classical criterion is proved here. Its converse — that a Borsuk map with a continuous logarithm on a bounded closed K forces a and b into one component of Kᶜ — is the deeper half, and is proved separately, in TauCeti/Analysis/Complex/PlaneSeparation/Basic.lean, as TauCeti.mem_connectedComponentIn_of_hasContinuousLogOn. Boundedness is essential there and is not assumed here. Nothing below uses that converse, and no statement below is phrased so as to presume it; in particular the naive route to it, through winding numbers of curves drawn inside K, is unavailable, since a compact connected set can separate the plane while containing no arc at all.

Roadmap role

Plane separation for Jordan curves was an open frontier item of layer L5 of TauCetiRoadmap/ConformalMapping/README.md, the Carathéodory boundary correspondence. TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton of TauCeti/Analysis/Complex/Conformal/Crosscut/Inside.lean avoids the plane-separation hypothesis entirely by taking IsPreconnected (K \ {f z₀}) instead, which IsJordanCurve.isPathConnected_sdiff_singleton discharges; Caratheodory.lean is now unconditional. The remaining open statement is frontier Ω ∩ closure A ∩ closure B ⊆ closure γ, the input TauCeti/Analysis/Complex/Conformal/Crosscut/BoundarySplit.lean names as missing before its dichotomy TauCeti.subset_or_subset_of_isPreconnected_frontier_image_sdiff can be fed a boundary arc.

The classical route to both runs through Janiszewski's theorem — two closed sets with connected intersection, neither of which separates a pair of points, have a union that does not separate it either — and Janiszewski is proved by translating "does not separate" into "the Borsuk map has a continuous logarithm" and gluing the two logarithms over the connected intersection. This file supplies that translation in the direction that holds without duality, together with the gluing; TauCeti/Analysis/Complex/PlaneSeparation/Basic.lean adds the converse direction and assembles the three into TauCeti.janiszewski.

The one statement below already phrased in the vocabulary of that development is TauCeti.mem_filledHull_or_mem_filledHull_of_not_hasContinuousLogOn: a bounded closed set on which the Borsuk map has no continuous logarithm encloses a or b in its filled hull. It reads the criterion through TauCeti.mem_filledHull_or_mem_filledHull_of_notMem_connectedComponentIn of TauCeti/Analysis/Normed/Module/FilledHull.lean, so a source of logarithm obstructions becomes a source of the enclosure hypothesis Conformal/Crosscut/Inside.lean consumes.

Coordination with upstream Mathlib

Mathlib has continuous branches of the logarithm on simply connected open sets (Complex.exists_continuousOn_eqOn_exp_comp of Mathlib/Analysis/Complex/BranchLogRoot.lean, which layer L3 consumes), but no predicate for a logarithm on an arbitrary set, no gluing theorem for logarithms, and no separation theory for the plane. 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, and it consumes no L0–L3 shim: its only complex-analytic input is the principal branch Complex.log on Complex.slitPlane.

Main results

• TauCeti.HasContinuousLogOn — the predicate, with TauCeti.hasContinuousLogOn_iff exposing it, and its closure properties TauCeti.HasContinuousLogOn.mul, .inv, .div, .mono, .congr.
• TauCeti.hasContinuousLogOn_of_mapsTo_slitPlane — a function landing in the slit plane has the principal logarithm.
• TauCeti.eq_of_isPreconnected_of_forall_exp_eq_one — a preconnected set of logarithms of 1 is a single point.
• TauCeti.HasContinuousLogOn.union — gluing: logarithms on two closed sets with preconnected overlap combine into one on the union.
• TauCeti.hasContinuousLogOn_sub_div_sub_of_norm_lt — the Borsuk map of two points closer to each other than to K has a logarithm on K.
• TauCeti.hasContinuousLogOn_sub_div_sub — the criterion: the Borsuk map of two points in one component of the complement of a closed set has a continuous logarithm on that set.
• TauCeti.mem_filledHull_or_mem_filledHull_of_not_hasContinuousLogOn — its separation-facing form: a bounded closed set admitting no such logarithm encloses one of the two points.

References

• K. Borsuk, Über Schnitte der euklidischen Räume, Math. Ann. 106 (1932).
• S. Janiszewski, Sur les coupures du plan faites par les continus, Prace Mat.-Fiz. 26 (1913).
• R. B. Burckel, An Introduction to Classical Complex Analysis I, §4 (logarithms and separation).
• J. R. Munkres, Topology, §61–63 (the separation theorems of the plane).

The predicate and its algebra

def TauCeti.HasContinuousLogOn {X : Type u_1} [TopologicalSpace X] (g : X → ℂ) (S : Set X) : Prop

HasContinuousLogOn g S asserts that the complex-valued function g admits a continuous logarithm on the set S: some h, continuous on S, satisfies exp (h x) = g x for every x ∈ S.

On a simply connected open set this holds for every zero-free continuous g, by Mathlib's Complex.exists_continuousOn_eqOn_exp_comp; on a general set — a compact subset of ℂ, say — it is a genuine restriction, and it is that restriction which detects separation of the plane.

Equations

• TauCeti.HasContinuousLogOn g S = ∃ (h : X → ℂ), ContinuousOn h S ∧ Set.EqOn (fun (x : X) => Complex.exp (h x)) g S

theorem TauCeti.hasContinuousLogOn_iff {X : Type u_1} [TopologicalSpace X] {g : X → ℂ} {S : Set X} : HasContinuousLogOn g S ↔ ∃ (h : X → ℂ), ContinuousOn h S ∧ ∀ x ∈ S, Complex.exp (h x) = g x

The defining property of TauCeti.HasContinuousLogOn, with the equality spelled out pointwise.

theorem TauCeti.HasContinuousLogOn.ne_zero {X : Type u_1} [TopologicalSpace X] {g : X → ℂ} {S : Set X} (h : HasContinuousLogOn g S) {x : X} (hx : x ∈ S) : g x ≠ 0

A function with a continuous logarithm has no zero, the exponential having none.

theorem TauCeti.HasContinuousLogOn.continuousOn {X : Type u_1} [TopologicalSpace X] {g : X → ℂ} {S : Set X} (h : HasContinuousLogOn g S) : ContinuousOn g S

A function with a continuous logarithm is itself continuous, being exp of one.

theorem TauCeti.HasContinuousLogOn.mono {X : Type u_1} [TopologicalSpace X] {g : X → ℂ} {S T : Set X} (h : HasContinuousLogOn g S) (hTS : T ⊆ S) : HasContinuousLogOn g T

Continuous logarithms restrict to subsets.

theorem TauCeti.HasContinuousLogOn.congr {X : Type u_1} [TopologicalSpace X] {g g' : X → ℂ} {S : Set X} (h : HasContinuousLogOn g S) (hg : Set.EqOn g g' S) : HasContinuousLogOn g' S

Having a continuous logarithm depends only on the values on the set.

theorem TauCeti.hasContinuousLogOn_const {X : Type u_1} [TopologicalSpace X] {S : Set X} {c : ℂ} (hc : c ≠ 0) : HasContinuousLogOn (fun (x : X) => c) S

A nonzero constant has a continuous logarithm, namely the constant principal logarithm.

theorem TauCeti.HasContinuousLogOn.mul {X : Type u_1} [TopologicalSpace X] {g g' : X → ℂ} {S : Set X} (h : HasContinuousLogOn g S) (h' : HasContinuousLogOn g' S) : HasContinuousLogOn (fun (x : X) => g x * g' x) S

Logarithms add under multiplication.

theorem TauCeti.HasContinuousLogOn.inv {X : Type u_1} [TopologicalSpace X] {g : X → ℂ} {S : Set X} (h : HasContinuousLogOn g S) : HasContinuousLogOn (fun (x : X) => (g x)⁻¹) S

Logarithms negate under inversion.

theorem TauCeti.HasContinuousLogOn.div {X : Type u_1} [TopologicalSpace X] {g g' : X → ℂ} {S : Set X} (h : HasContinuousLogOn g S) (h' : HasContinuousLogOn g' S) : HasContinuousLogOn (fun (x : X) => g x / g' x) S

Logarithms subtract under division.

theorem TauCeti.hasContinuousLogOn_of_mapsTo_slitPlane {X : Type u_1} [TopologicalSpace X] {g : X → ℂ} {S : Set X} (hg : ContinuousOn g S) (hS : ∀ x ∈ S, g x ∈ Complex.slitPlane) : HasContinuousLogOn g S

A function landing in the slit plane has the principal logarithm. This is the only source of logarithms that does not come from another logarithm, and everything below is built on it.

Gluing along a connected overlap

theorem TauCeti.eq_of_isPreconnected_of_forall_exp_eq_one {P : Set ℂ} (hP : IsPreconnected P) (h : ∀ w ∈ P, Complex.exp w = 1) {w₁ w₂ : ℂ} (h₁ : w₁ ∈ P) (h₂ : w₂ ∈ P) : w₁ = w₂

A preconnected set of logarithms of 1 is a single point. Every such logarithm is an integer multiple of 2 * π * I, and two distinct multiples are at distance at least 2 * π, so Complex.exp ⁻¹' {1} is a discrete subset of ℂ; a preconnected set inside it is therefore a single point, by IsPreconnected.constant_of_mapsTo applied to the identity.

theorem TauCeti.HasContinuousLogOn.union {X : Type u_1} [TopologicalSpace X] {g : X → ℂ} {S T : Set X} (hS : IsClosed S) (hT : IsClosed T) (hST : IsPreconnected (S ∩ T)) (h : HasContinuousLogOn g S) (h' : HasContinuousLogOn g T) : HasContinuousLogOn g (S ∪ T)

Continuous logarithms glue along a preconnected overlap. Two logarithms of g differ, on the overlap, by a logarithm of 1; that difference is constant there by TauCeti.eq_of_isPreconnected_of_forall_exp_eq_one, so shifting one logarithm by the constant makes the two agree on S ∩ T and define a single function, continuous on the union because both pieces are closed.

The overlap is only asked to be preconnected, so the disjoint case is allowed: there the two logarithms are glued unchanged.

The Borsuk map of a pair of points

theorem TauCeti.hasContinuousLogOn_sub_div_sub_of_norm_lt {K : Set ℂ} {w w' : ℂ} (h : ∀ z ∈ K, ‖w - w'‖ < ‖z - w'‖) : HasContinuousLogOn (fun (z : ℂ) => (z - w) / (z - w')) K

The Borsuk map of two points nearer each other than the set has a logarithm there. If every z ∈ K is further from w' than w is, then (z - w) / (z - w') = 1 + (w' - w) / (z - w') lies within distance 1 of 1, hence in the slit plane, where the principal logarithm is available.

theorem TauCeti.hasContinuousLogOn_sub_div_sub {K : Set ℂ} {a b : ℂ} (hK : IsClosed K) (hb : b ∈ connectedComponentIn Kᶜ a) : HasContinuousLogOn (fun (z : ℂ) => (z - a) / (z - b)) K

The Borsuk-map criterion, sufficient direction. If b lies in the connected component of a in the complement of a closed set K, then the Borsuk map z ↦ (z - a) / (z - b) has a continuous logarithm on K.

Contrapositively: if a closed set K carries no continuous logarithm of the Borsuk map of a and b, then b ∉ connectedComponentIn Kᶜ a; for a, b outside K that says the two points lie in different components of Kᶜ, and otherwise one of them lies in K itself.

The proof moves the second point rather than constructing the logarithm. The set of points w of Kᶜ for which z ↦ (z - a) / (z - w) has a logarithm on K is open, because displacing w by less than half its distance to K multiplies the Borsuk map by a factor covered by TauCeti.hasContinuousLogOn_sub_div_sub_of_norm_lt; the same estimate run backwards makes the complementary set of Kᶜ open too. Since a itself is in the first set — its Borsuk map is the constant 1 — and the component of a is preconnected, the component lies in it.

theorem TauCeti.mem_filledHull_or_mem_filledHull_of_not_hasContinuousLogOn {K : Set ℂ} {a b : ℂ} (hK : IsClosed K) (hKb : Bornology.IsBounded K) (h : ¬HasContinuousLogOn (fun (z : ℂ) => (z - a) / (z - b)) K) : a ∈ filledHull K ∨ b ∈ filledHull K

A bounded closed set with no continuous logarithm of a Borsuk map encloses one of the two points. This is TauCeti.hasContinuousLogOn_sub_div_sub read through TauCeti.mem_filledHull_or_mem_filledHull_of_notMem_connectedComponentIn: failure of the logarithm gives b ∉ connectedComponentIn Kᶜ a, so either one of the two points lies in K, and hence in the filled hull outright, or they lie in different components of Kᶜ, of which at most one can be the unbounded component of a bounded set's complement.

It is the form in which an obstruction to a logarithm delivers the enclosure hypothesis of TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton.