Preconnected approach regions for Jordan domains

A Jordan domain has preconnected approach regions at every boundary point. The proof uses Janiszewski's theorem (TauCeti.janiszewski) and one arc lemma, avoiding the Jordan curve theorem and Schoenflies.

Given a ∈ frontier U with U a Jordan domain, take an open arc W ⊆ frontier U ∩ ball a r through a whose complement frontier U \ W is closed and preconnected. Set S := frontier U and T := sphere a r ∪ (frontier U \ W). Then S ∩ T = frontier U \ W is preconnected, S does not separate points of U, and T does not separate points of ball a ρ for small ρ; Janiszewski puts both in one component of (S ∪ T)ᶜ ⊆ U ∩ ball a r.

Combined with injOn_closedBall_of_isPreconnected_image_approach from Inverse/BoundaryCluster.lean, this gives injectivity on the closed disc for the Riemann map of a Jordan domain, and with closureHomeomorph from BoundaryCorrespondence.lean, the homeomorphism of closures.

Input

• TauCeti.IsJordanCurve.exists_isCompact_isPreconnected_notMem_sdiff_subset_ball (JordanCurve/SmallArc.lean) — a Jordan curve admits a compact preconnected arc missing any given point, whose complement lies in a given ball.

Main results

• TauCeti.IsJordanDomain.isPreconnectedApproachAt — a Jordan domain has preconnected approach regions at every boundary point.
• TauCeti.injOn_closedBall_of_isJordanCurve_frontier — injectivity on the closed disc for the Riemann map, Jordan case.
• TauCeti.exists_homeomorph_closedBall_closure_of_isJordanCurve_frontier — the Riemann map extends to a homeomorphism of the closures.

References

• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).

Jordan domains

theorem TauCeti.IsJordanDomain.exists_isPreconnected_inter_ball_subset {U : Set ℂ} {a : ℂ} (hU : IsJordanDomain U) (ha : a ∈ frontier U) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∃ C ⊆ U ∩ Metric.ball a ε, IsPreconnected C ∧ U ∩ Metric.ball a δ ⊆ C

A Jordan domain is locally connected from within at each boundary point. The arc lemma supplies the closed complementary arc, the Janiszewski step does the rest.

theorem TauCeti.IsJordanDomain.isPreconnectedApproachAt {U : Set ℂ} {a : ℂ} (hU : IsJordanDomain U) (ha : a ∈ frontier U) : IsPreconnectedApproachAt U a

A Jordan domain has preconnected approach regions at every boundary point.

theorem TauCeti.IsJordanDomain.injOn_closedBall_of_conformal {f F : ℂ → ℂ} {c : ℂ} {r : ℝ} (hr : 0 < r) (hfd : DifferentiableOn ℂ f (Metric.ball c r)) (hfi : Set.InjOn f (Metric.ball c r)) (hFc : ContinuousOn F (Metric.closedBall c r)) (hFf : Set.EqOn F f (Metric.ball c r)) (hJ : IsJordanDomain (f '' Metric.ball c r)) : Set.InjOn F (Metric.closedBall c r)

Conformal injectivity on the closed disc when the image is a Jordan domain. Feeds IsJordanDomain.isPreconnectedApproachAt into injOn_closedBall_of_isPreconnected_image_approach.

theorem TauCeti.injOn_closedBall_of_isJordanCurve_frontier {f F : ℂ → ℂ} {c : ℂ} {r : ℝ} (hr : 0 < r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hinj : Set.InjOn f (Metric.ball c r)) (hb : Bornology.IsBounded (f '' Metric.ball c r)) (hJf : IsJordanCurve (frontier (f '' Metric.ball c r))) (hFc : ContinuousOn F (Metric.closedBall c r)) (hFf : Set.EqOn F f (Metric.ball c r)) : Set.InjOn F (Metric.closedBall c r)

Boundary injectivity, Jordan case, in the hypothesis shape of TauCeti.exists_continuousOn_closedBall_eqOn_of_isJordanCurve_frontier.

theorem TauCeti.exists_homeomorph_closedBall_closure_of_isJordanCurve_frontier {Ω : Set ℂ} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (hΩJ : IsJordanCurve (frontier Ω)) : ∃ (g : ℂ → ℂ), ContinuousOn g (Metric.closedBall 0 1) ∧ DifferentiableOn ℂ g (Metric.ball 0 1) ∧ Set.BijOn g (Metric.ball 0 1) Ω ∧ ∃ (e : ↑(Metric.closedBall 0 1) ≃ₜ ↑(closure Ω)), ∀ (z : ↑(Metric.closedBall 0 1)), ↑(e z) = g ↑z

The Riemann map of a Jordan domain extends to a homeomorphism of the closures.