Boundary uniqueness across a circular arc #
A holomorphic function on a disc that extends continuously to a relatively open piece of the
bounding circle and is constant there is constant on the whole disc. That piece is
V ∩ sphere c r for an open V ⊆ ℂ meeting the circle, and no hypothesis whatever is placed on
the function along the rest of the circle. Nothing forces V ∩ sphere c r to be connected, so the
declarations are named after that literal hypothesis, inter_sphere; the prose below calls such a
set a boundary arc, the case of interest, but no arc parameterization is assumed.
The proof is Painlevé removability, not the identity principle applied to the boundary: the
boundary values are a set with no limit point inside the disc, so no uniqueness statement about
the disc alone can see them. Instead the function is continued past the arc by the trivial branch.
On a small ball Ω centred at a point of the arc, glue f - a inside the closed disc to the
constant 0 outside it. The two branches agree on Ω ∩ sphere c r, which is exactly the frontier
of the closed disc met by Ω, so the glued function is continuous on Ω; it is holomorphic off
the circle; and TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_sphere — the
circle case of Painlevé removability from Conformal/Removability/Circle.lean — makes it
holomorphic on all of Ω. It vanishes identically on the part of Ω outside the closed disc,
which is open and nonempty because Ω straddles the circle, so the identity principle kills it on
Ω and hence on the nonempty open set Ω ∩ ball c r; a second application of the identity
principle, this time inside ball c r, propagates f = a to the whole disc.
The point of the statement is its contrapositive: a function that is not the constant a on the
disc is not the constant a on any boundary arc, so — for an injective map, which is constant
nowhere — every boundary fibre has empty interior in the circle.
What this does and does not supply towards L5 #
This is a prerequisite for layer L5 of the conformal-mapping roadmap, not that layer's
boundary-injectivity step. Carathéodory's proof that the extension of a Riemann map of a Jordan
domain is injective on frontier argues by contradiction in two halves: two identified boundary
points cut the circle into two arcs, and the Jordan-curve geometry of the image forces the
extension to be constant on one of them; that constancy is then impossible. Only the second half
is proved here. Producing the constant arc from an identification of two boundary points is a
Jordan-curve argument about the image, and is not proved here, nor is the singleton
cluster-set property that produces the continuous extension in the first place —
Conformal/ClusterSet.lean records both as still missing, which is why
TauCeti.injOn_closure_of_injOn_frontier there carries boundary injectivity as a hypothesis. So no
boundary-injectivity claim is discharged by this file; what it adds is the analytic
non-degeneracy input that the two-arc route would consume.
Conformal/Jordan/Approach.lean proves boundary injectivity by a different route (Janiszewski
and preconnected approach regions) and does not consume this file.
Main results #
TauCeti.eqOn_const_ball_of_eqOn_const_inter_sphere— a holomorphic function continuous up to a boundary arc and constant on it is constant on the disc.TauCeti.eqOn_ball_of_eqOn_inter_sphere— the two-function form: holomorphic functions agreeing on a boundary arc agree on the disc.TauCeti.not_eqOn_const_inter_sphere_of_not_eqOn_const_ballandTauCeti.interior_setOf_eq_eq_empty_of_not_eqOn_const_ball— the contrapositive, for a function that is not that constant on the disc, in the two forms.TauCeti.not_eqOn_const_inter_sphere_of_injOnandTauCeti.interior_setOf_eq_eq_empty_of_injOn— the roadmap-facing corollaries for a conformal map, which is constant on no boundary arc and each of whose boundary fibres therefore has empty interior in the circle.
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 neither a boundary uniqueness theorem of this shape nor Painlevé removability. So this file is new Lean formalization rather than a temporary shim; it consumes only the L4 removability layer, which is likewise new.
References #
- L. V. Ahlfors, Complex Analysis, Ch. 6, §1.4 (the reflection and removability circle of ideas).
- Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
- C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).
Boundary uniqueness across a circular arc. Let f be holomorphic on ball c r, continuous
up to the part of the closed disc lying in an open set V, and equal to the constant a on the
arc V ∩ sphere c r. If that arc is nonempty, then f is the constant a on the whole disc.
No hypothesis is placed on f along the rest of the circle: the arc alone determines the function.
The proof continues f - a past the arc by 0 and applies Painlevé removability across the
circle, then the identity principle twice; see the module docstring.
Boundary uniqueness on an arc, two-function form. Holomorphic functions on ball c r that
extend continuously to a nonempty boundary arc V ∩ sphere c r and agree there agree on the whole
disc. This is TauCeti.eqOn_const_ball_of_eqOn_const_inter_sphere applied to the difference.
A function nonconstant on the disc is constant on no boundary arc. If f is holomorphic on
ball c r, continuous up to a nonempty boundary arc V ∩ sphere c r, and is not the constant a
on the disc, then it is not the constant a on that arc.
This is the contrapositive of TauCeti.eqOn_const_ball_of_eqOn_const_inter_sphere; injectivity of
f is not needed, only its failure to be this one constant.
The boundary fibres of a nonconstant function contain no arc. For f holomorphic on
ball c r, continuous on the closed disc and not the constant a on the disc, the set of boundary
points at which f takes the value a has empty interior in the circle.
This is the relative-topology packaging of
TauCeti.not_eqOn_const_inter_sphere_of_not_eqOn_const_ball: a nonempty open subset of
sphere c r is precisely a nonempty arc V ∩ sphere c r for an open V ⊆ ℂ.
A conformal map is constant on no boundary arc. If f is holomorphic and injective on
ball c r and continuous up to a nonempty boundary arc V ∩ sphere c r, it takes no value
constantly on that arc.
This is the roadmap-facing corollary of
TauCeti.not_eqOn_const_inter_sphere_of_not_eqOn_const_ball, an injective map being constant
nowhere. It is the boundary non-degeneracy that layer L5 of the conformal-mapping roadmap needs;
see the module docstring for what still separates it from boundary injectivity.
The boundary fibres of a conformal map contain no arc. For f holomorphic and injective on
ball c r and continuous on the closed disc, the set of boundary points at which f takes a fixed
value has empty interior in the circle.
This is the roadmap-facing corollary of
TauCeti.interior_setOf_eq_eq_empty_of_not_eqOn_const_ball.