Documentation

TauCeti.Analysis.Complex.Conformal.Crosscut.Path

A finite-length image crosscut as a path #

Conformal/Crosscut/EndpointLimit.lean proves that the image of a circular crosscut of finite length has an honest limit at each of its two ends, and identifies its closure set-theoretically as the open image crosscut together with those ends. This file packages the same curve as a Path: its range is exactly that closure, it follows the usual angular parametrisation in its interior, and that interior is injective when the holomorphic map is injective on the disc.

This is a topological input to layer L5 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md), the Carathéodory boundary correspondence. The next separation step joins a closed image crosscut to one of the two arcs that its endpoints cut from the Jordan boundary. The set-level description of the closure does not by itself supply the continuous parametrisation that such an argument needs; the path below does.

Construction #

Write

a = arg (c - ζ) - arccos (ρ / (2r)) and b = arg (c - ζ) + arccos (ρ / (2r)).

The open interval Ioo a b parametrises ball c r ∩ sphere ζ ρ. At every point of its frontier, the endpoint-limit theorem gives a limit of f along the crosscut. Composing with circleMap turns those into limits of the angular composite g = f ∘ circleMap ζ ρ at a and at b, which is exactly the data TauCeti.Path.ofContinuousOnIoo of TauCeti/Topology/Path/ExtendIoo.lean consumes: a function continuous on an open interval with a limit at each end traces a path between those two limits, whose range is the closure of the curve (TauCeti.Path.range_ofContinuousOnIoo) and which follows g along AffineMap.lineMap a b : [0, 1] → [a, b] in the interior (TauCeti.Path.ofContinuousOnIoo_apply_of_mem_Ioo). All the holomorphy is spent before that point, in producing the two endpoint limits.

This construction does not need injectivity. When f is injective on the disc, a companion theorem also places the endpoints on the image frontier and shows that only the two endpoints can be identified. Interior injectivity uses only the injectivity of f, Mathlib's Complex.injOn_circleMap_of_abs_sub_le, the fact that b - a < 2π, and the injectivity of AffineMap.lineMap a b; the last step, that a curve injective on the interior and avoiding both endpoint values there can repeat only between its endpoints, is TauCeti.eq_or_eq_endpoints_of_notMem_of_forall_mem_Ioo of the same file.

Main result #

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. Mathlib supplies Path and the injectivity of circleMap on an interval shorter than a full turn; the extension of a curve across the two ends of an open interval is packaged as a path in TauCeti/Topology/Path/ExtendIoo.lean. Mathlib has no boundary-crosscut or endpoint-limit result. No Mathlib source is vendored.

References #

source
theorem TauCeti.exists_path_range_eq_closure_image_ball_inter_sphere {f : ℂ → ℂ} {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) :
∃ (u : ℂ) (v : ℂ) (γ : Path u v), Set.range ⇑γ = closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ∧ Filter.Tendsto f (nhdsWithin (circleMap ζ ρ ((c - ζ).arg - Real.arccos (ρ / (2 * r)))) (Metric.ball c r ∩ Metric.sphere ζ ρ)) (nhds u) ∧ Filter.Tendsto f (nhdsWithin (circleMap ζ ρ ((c - ζ).arg + Real.arccos (ρ / (2 * r)))) (Metric.ball c r ∩ Metric.sphere ζ ρ)) (nhds v) ∧ ∀ t ∈ Set.Ioo 0 1, γ t = f (circleMap ζ ρ ((AffineMap.lineMap ((c - ζ).arg - Real.arccos (ρ / (2 * r))) ((c - ζ).arg + Real.arccos (ρ / (2 * r)))) ↑t))

A finite-length circular image crosscut is the interior of a path. Let ζ lie on sphere c r, and let 0 < ρ < 2r, so that ball c r ∩ sphere ζ ρ is a genuine circular crosscut. If f is holomorphic on ball c r and the image crosscut has finite TauCeti.circleImageLength, then there are endpoints u, v and a path from u to v whose range is exactly closure (f '' (ball c r ∩ sphere ζ ρ)) and which has the usual angular parametrisation on the open unit interval.

The two additional Tendsto conclusions identify u and v with the endpoint limits of the crosscut. No injectivity is needed for this construction. The companion theorem TauCeti.exists_path_range_eq_closure_image_ball_inter_sphere_of_injOn records the stronger frontier and no-repetition properties available when f is injective.

source
theorem TauCeti.exists_path_range_eq_closure_image_ball_inter_sphere_of_injOn {f : ℂ → ℂ} {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hinj : Set.InjOn f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) :
∃ (u : ℂ) (v : ℂ) (γ : Path u v), Set.range ⇑γ = closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ∧ Filter.Tendsto f (nhdsWithin (circleMap ζ ρ ((c - ζ).arg - Real.arccos (ρ / (2 * r)))) (Metric.ball c r ∩ Metric.sphere ζ ρ)) (nhds u) ∧ Filter.Tendsto f (nhdsWithin (circleMap ζ ρ ((c - ζ).arg + Real.arccos (ρ / (2 * r)))) (Metric.ball c r ∩ Metric.sphere ζ ρ)) (nhds v) ∧ u ∈ frontier (f '' Metric.ball c r) ∧ v ∈ frontier (f '' Metric.ball c r) ∧ (∀ ⦃x y : ↑unitInterval⦄, γ x = γ y → x = y ∨ x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0) ∧ ∀ t ∈ Set.Ioo 0 1, γ t = f (circleMap ζ ρ ((AffineMap.lineMap ((c - ζ).arg - Real.arccos (ρ / (2 * r))) ((c - ζ).arg + Real.arccos (ρ / (2 * r)))) ↑t))

An injective finite-length circular image crosscut has no repetitions except possibly at its endpoints. Under the hypotheses of TauCeti.exists_path_range_eq_closure_image_ball_inter_sphere, assume additionally that f is injective on ball c r. Then the endpoints of the resulting path lie on frontier (f '' ball c r) and remain identified by their endpoint limits, its interior is injective, and no endpoint value occurs in the interior. Thus the only possible repeated value is a common value of the two endpoints.

The endpoints need not be distinct: before the Carathéodory boundary theorem, the hypotheses do not exclude an image crosscut closing up at the boundary.