Injectivity of a monotone conformal extension

This file isolates the remaining topological input in the injectivity half of Carathéodory's boundary correspondence. Let F be continuous on a closed disc, holomorphic and injective on its interior. If every point fibre of the boundary restriction is connected, then F is injective on the boundary and hence on the whole closed disc.

The proof joins two existing parts of the conformal-mapping development. Boundary uniqueness in TauCeti/Analysis/Complex/Conformal/ArcConstancy.lean says that a conformal map is constant on no relative open arc of the bounding circle, so each boundary fibre has empty interior. The monotone Jordan-curve theorem in TauCeti/Topology/JordanCurve/Monotone.lean then turns connectedness of the fibres into injectivity. Finally, TauCeti.injOn_closure_of_injOn_frontier propagates boundary injectivity across the closed disc, since a boundary value of a conformal map cannot also be an interior value.

For the layer L5 Carathéodory milestone, the continuous extension is supplied by the length–area and plane-separation argument. The result here shows that upgrading it to the requested homeomorphism of closures needs exactly the monotonicity of its boundary restriction; it does not assume or assert that monotonicity for an arbitrary continuous extension.

Main results

• TauCeti.injOn_sphere_of_isPreconnected_boundary_fiber — a monotone boundary restriction of a conformal disc map is injective.
• TauCeti.injOn_sphere_iff_isPreconnected_boundary_fiber — monotonicity of the boundary restriction is exactly its injectivity.
• TauCeti.injOn_closedBall_of_isPreconnected_boundary_fiber — the extension is injective on the closed disc.
• TauCeti.bijOn_closedBall_closure_image_of_isPreconnected_boundary_fiber — consequently it is a bijection from the closed disc onto the closure of the conformal image; the existing TauCeti.closureHomeomorph packages this bijection as a homeomorphism.

References

• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.

theorem TauCeti.injOn_sphere_of_isPreconnected_boundary_fiber {c : ℂ} {r : ℝ} {F : ℂ → ℂ} (hr : 0 < r) (hcont : ContinuousOn F (Metric.closedBall c r)) (hdiff : DifferentiableOn ℂ F (Metric.ball c r)) (hinj : Set.InjOn F (Metric.ball c r)) (hpre : ∀ (a : ℂ), IsPreconnected {z : ↑(Metric.sphere c r) | F ↑z = a}) : Set.InjOn F (Metric.sphere c r)

A conformal disc map with a monotone boundary restriction is injective on the circle. Suppose F is continuous on closedBall c r, holomorphic and injective on ball c r, and every point fibre of its restriction to sphere c r is preconnected. Then the restriction is injective.

The fibre-interior hypothesis of TauCeti.IsJordanCurve.injective_of_isPreconnected_fiber_of_interior_fiber_eq_empty is exactly TauCeti.interior_setOf_eq_eq_empty_of_injOn, the boundary uniqueness theorem for a conformal map.

theorem TauCeti.injOn_sphere_iff_isPreconnected_boundary_fiber {c : ℂ} {r : ℝ} {F : ℂ → ℂ} (hr : 0 < r) (hcont : ContinuousOn F (Metric.closedBall c r)) (hdiff : DifferentiableOn ℂ F (Metric.ball c r)) (hinj : Set.InjOn F (Metric.ball c r)) : Set.InjOn F (Metric.sphere c r) ↔ ∀ (a : ℂ), IsPreconnected {z : ↑(Metric.sphere c r) | F ↑z = a}

For a conformal extension, boundary monotonicity is equivalent to boundary injectivity. Boundary uniqueness makes every point fibre interiorless, so TauCeti.IsJordanCurve.injective_iff_isPreconnected_fiber_of_interior_fiber_eq_empty applies to the restriction of F to sphere c r.

This equivalence makes the outstanding geometric input in the Carathéodory injectivity argument precise: proving that the boundary fibres are preconnected is neither weaker nor stronger than the required boundary injectivity once the conformal and continuity hypotheses are available.

theorem TauCeti.injOn_closedBall_of_isPreconnected_boundary_fiber {c : ℂ} {r : ℝ} {F : ℂ → ℂ} (hr : 0 < r) (hcont : ContinuousOn F (Metric.closedBall c r)) (hdiff : DifferentiableOn ℂ F (Metric.ball c r)) (hinj : Set.InjOn F (Metric.ball c r)) (hpre : ∀ (a : ℂ), IsPreconnected {z : ↑(Metric.sphere c r) | F ↑z = a}) : Set.InjOn F (Metric.closedBall c r)

A conformal disc map with a monotone boundary restriction is injective on the closed disc. Boundary injectivity comes from TauCeti.injOn_sphere_of_isPreconnected_boundary_fiber; the interior and boundary images are disjoint by conformal properness, so TauCeti.injOn_closure_of_injOn_frontier gives injectivity on the closure.

theorem TauCeti.bijOn_closedBall_closure_image_of_isPreconnected_boundary_fiber {c : ℂ} {r : ℝ} {F : ℂ → ℂ} (hr : 0 < r) (hcont : ContinuousOn F (Metric.closedBall c r)) (hdiff : DifferentiableOn ℂ F (Metric.ball c r)) (hinj : Set.InjOn F (Metric.ball c r)) (hpre : ∀ (a : ℂ), IsPreconnected {z : ↑(Metric.sphere c r) | F ↑z = a}) : Set.BijOn F (Metric.closedBall c r) (closure (F '' Metric.ball c r))

A monotone conformal extension is a bijection of the closed disc with the closure of its image. This is the set-level conclusion needed to instantiate TauCeti.closureHomeomorph. Surjectivity is continuity on the compact closed disc; injectivity is TauCeti.injOn_closedBall_of_isPreconnected_boundary_fiber.