Borsuk's separation criterion and Janiszewski's theorem

Two points a, b of the plane lie in the same connected component of the complement of a compact set K exactly when the Borsuk map z ↦ (z - a) / (z - b) admits a continuous logarithm on K. TauCeti/Analysis/Complex/ContinuousLog/Basic.lean introduces the predicate TauCeti.HasContinuousLogOn and proves the implication that needs no duality — a logarithm exists as soon as the two points are joined inside Kᶜ (TauCeti.hasContinuousLogOn_sub_div_sub) — and records the converse as the missing input. This file proves the converse, TauCeti.mem_connectedComponentIn_of_hasContinuousLogOn, and reads the resulting equivalence off as Janiszewski's theorem: two bounded closed sets whose intersection is preconnected, neither of which separates a from b, have a union that does not separate them either.

The argument

Boundedness of K is essential: the real axis separates i from -i, yet the Borsuk map of that pair is a homeomorphism of ℝ onto the circle minus a point and so has a logarithm. What boundedness buys is that at most one component of Kᶜ is unbounded (TauCeti.connectedComponentIn_compl_eq_of_unbounded_component), so of two points in different components at least one — say a, after exchanging them and inverting the Borsuk map — has a bounded component V.

Suppose then that the Borsuk map has a logarithm h on K. Extend h to a continuous H : ℂ → ℂ by Tietze and put G = exp ∘ H: a nowhere-vanishing continuous function on the whole plane agreeing with (z - a) / (z - b) on K. The component V is open, its frontier lies in K (TauCeti.frontier_connectedComponentIn_subset_compl), and b misses closure V = V ∪ frontier V. The globally continuous functions z ↦ G z * (z - b) and z ↦ z - a agree on frontier (closure V) ⊆ frontier V ⊆ K, because there G z * (z - b) = ((z - a) / (z - b)) * (z - b) = z - a. Therefore Continuous.piecewise shows that their piecewise combination

Φ = (closure V).piecewise (fun z => G z * (z - b)) (fun z => z - a)

is continuous, and it vanishes nowhere: on closure V because G is zero-free and b ∉ closure V, off closure V because a ∈ V.

A zero-free continuous function on the plane has a continuous logarithm by Complex.exists_continuousOn_eqOn_exp_comp, hence so does its restriction to any circle. But V is bounded, so a large enough circle about a misses closure V, and there Φ z = z - a, which has no continuous logarithm on a circle about a (TauCeti.not_hasContinuousLogOn_sub_sphere) — the classical winding obstruction, proved here by following t ↦ h (a + r * exp (t * I)) - t * I - log r once around and finding it both constant and shifted by 2 * π * I. That contradiction is the theorem.

Nothing in the argument looks at curves inside K, or asks K to be connected, locally connected, or to contain an arc; K enters only through the frontier of one component of its complement.

Roadmap role

Plane separation for Jordan curves was the 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. TauCeti/Analysis/Complex/ContinuousLog/Basic.lean names the remaining open statement on the classical route through Janiszewski's theorem — the converse direction — and this file supplies it, so TauCeti.janiszewski is available to that route as well.

Mathlib has no separation theory for the plane and no Jordan curve theorem, and layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort. The lifting of a zero-free continuous function through Complex.exp is supplied by Mathlib's Complex.exists_continuousOn_eqOn_exp_comp.

Main results

• TauCeti.not_hasContinuousLogOn_sub_sphere — z ↦ z - a has no continuous logarithm on a circle centred at a.
• TauCeti.mem_connectedComponentIn_of_hasContinuousLogOn — Borsuk's separation theorem: a continuous logarithm of the Borsuk map on a bounded closed set puts the two points in one component of the complement.
• TauCeti.hasContinuousLogOn_sub_div_sub_iff — the resulting equivalence.
• TauCeti.janiszewski — Janiszewski's theorem.

References

• K. Borsuk, Über Schnitte der euklidischen Räume, Math. Ann. 106 (1932), 239–248.
• 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.
• J. R. Munkres, Topology, §61–63.

The winding obstruction on a circle

theorem TauCeti.not_hasContinuousLogOn_sub_sphere {r : ℝ} (hr : 0 ≤ r) (a : ℂ) : ¬HasContinuousLogOn (fun (z : ℂ) => z - a) (Metric.sphere a r)

A circle carries no continuous logarithm of the map to its centre. This is the winding obstruction used in the plane-separation argument.

Borsuk's separation theorem

theorem TauCeti.mem_connectedComponentIn_of_hasContinuousLogOn {K : Set ℂ} {a b : ℂ} (hK : IsClosed K) (hKb : Bornology.IsBounded K) (hlog : HasContinuousLogOn (fun (z : ℂ) => (z - a) / (z - b)) K) : b ∈ connectedComponentIn Kᶜ a

Borsuk's separation theorem. If the Borsuk map z ↦ (z - a) / (z - b) of two points outside a bounded closed set K ⊆ ℂ has a continuous logarithm on K, then K does not separate them: b lies in the connected component of a in Kᶜ.

That the two points lie outside K is not assumed: the Borsuk map vanishes at a and, by the division convention, at b as well, so a logarithm on K already excludes both from K.

This is the converse of TauCeti.hasContinuousLogOn_sub_div_sub, and the direction that fails without boundedness — the real axis separates i from -i while carrying a logarithm of their Borsuk map.

theorem TauCeti.hasContinuousLogOn_sub_div_sub_iff {K : Set ℂ} {a b : ℂ} (hK : IsClosed K) (hKb : Bornology.IsBounded K) : HasContinuousLogOn (fun (z : ℂ) => (z - a) / (z - b)) K ↔ b ∈ connectedComponentIn Kᶜ a

The Borsuk criterion. For two points outside a bounded closed set K ⊆ ℂ, the Borsuk map z ↦ (z - a) / (z - b) has a continuous logarithm on K exactly when K fails to separate the two points; both sides already force a and b outside K. The easy direction is TauCeti.hasContinuousLogOn_sub_div_sub, the hard one TauCeti.mem_connectedComponentIn_of_hasContinuousLogOn.

Janiszewski's theorem

theorem TauCeti.janiszewski {a b : ℂ} {S T : Set ℂ} (hS : IsClosed S) (hT : IsClosed T) (hSb : Bornology.IsBounded S) (hTb : Bornology.IsBounded T) (hST : IsPreconnected (S ∩ T)) (hSsep : b ∈ connectedComponentIn Sᶜ a) (hTsep : b ∈ connectedComponentIn Tᶜ a) : b ∈ connectedComponentIn (S ∪ T)ᶜ a

Janiszewski's theorem. If two bounded closed subsets S, T of the plane have preconnected intersection and neither separates a from b, then their union does not separate them either.