Continuous logarithms on simple arcs

A zero-free continuous complex-valued function on a simple arc has a continuous logarithm. Here an arc is presented as the range of a path γ : Path x y whose parametrization is an embedding; the main theorem is TauCeti.hasContinuousLogOn_range_of_isEmbedding_path.

The proof extends γ constantly to ℝ and lifts g ∘ γ.extend through the covering map Complex.exp : ℂ → ℂ \ {0}. Since ℝ is simply connected, Mathlib's Complex.exists_continuousOn_eqOn_exp_comp supplies the lift, and the embedding hypothesis makes the parametrization a homeomorphism onto the range, along which the lift descends to the arc itself. The Borsuk-map specialization TauCeti.hasContinuousLogOn_sub_div_sub_range_of_injective_path records the form used by plane separation; there the embedding comes for free, an injective path from the compact unit interval into a Hausdorff space being a closed embedding. No formalization is vendored.

Roadmap role

The Carathéodory enclosure step (layer L5 of TauCetiRoadmap/ConformalMapping/README.md) is now unconditional: the preconnectedness/winding-number route in TauCeti/Analysis/Complex/Conformal/Crosscut/Inside.lean discharges it without plane separation. The classical separation route — Borsuk's criterion (PR #4701) plus arc nonseparation — remains relevant for future work. This file supplies the logarithm construction needed for that route: applying TauCeti.hasContinuousLogOn_sub_div_sub_range_of_injective_path shows that any two points off a simple arc lie in the same component of its complement.

This is deliberately stated for paths in an arbitrary topological space, since neither the lifting argument nor descent to the range uses planar geometry. The logarithm is still complex-valued, as required by TauCeti.HasContinuousLogOn and by the L5 Borsuk-map consumer.

Main results

• TauCeti.hasContinuousLogOn_range_of_isEmbedding_path — every zero-free continuous function on the range of a path with embedded parametrization has a continuous logarithm.
• TauCeti.hasContinuousLogOn_sub_div_sub_range_of_injective_path — the Borsuk map of two points outside a simple complex arc has a continuous logarithm on that arc.

References

• S. Janiszewski, Sur les coupures du plan faites par les continus, Prace Mat.-Fiz. 26 (1913).
• J. R. Munkres, Topology, §61–63.

theorem TauCeti.hasContinuousLogOn_range_of_isEmbedding_path {X : Type u_1} [TopologicalSpace X] {x y : X} {g : X → ℂ} (γ : Path x y) (hγe : Topology.IsEmbedding ⇑γ) (hg : ContinuousOn g (Set.range ⇑γ)) (hzero : ∀ z ∈ Set.range ⇑γ, g z ≠ 0) : HasContinuousLogOn g (Set.range ⇑γ)

A zero-free continuous function on a simple arc has a continuous logarithm. Let γ be a path whose parametrization is an embedding. If g is continuous and nonzero on range γ, then there is a function continuous on range γ whose exponential is g there.

theorem TauCeti.hasContinuousLogOn_sub_div_sub_range_of_injective_path {p q a b : ℂ} (γ : Path p q) (hγ : Function.Injective ⇑γ) (ha : a ∉ Set.range ⇑γ) (hb : b ∉ Set.range ⇑γ) : HasContinuousLogOn (fun (z : ℂ) => (z - a) / (z - b)) (Set.range ⇑γ)

The Borsuk map of two points off a simple complex arc has a continuous logarithm on the arc. The two nonmembership hypotheses say exactly that the numerator and the denominator of z ↦ (z - a) / (z - b) do not vanish along the arc.

Together with Borsuk's converse criterion for bounded closed sets, this is the standard proof that an arc does not separate the plane.