Boundedness of smooth Jordan domains

The boundary representation in SmoothJordanDomain, together with convexity, forces the represented carrier to be the bounded side of its Jordan trace. Canonical orientation supplies winding number one throughout the carrier; the scalar Cauchy transform then tends to zero at infinity, ruling out an unbounded carrier.

theorem SmoothJordanDomain.isBounded_carrier (Omega : SmoothJordanDomain) : Bornology.IsBounded Omega.carrier

Every represented smooth convex Jordan carrier is bounded.

theorem SmoothJordanDomain.isCompact_closure (Omega : SmoothJordanDomain) : IsCompact (closure Omega.carrier)

The closure of every represented smooth convex Jordan carrier is compact.

theorem SmoothJordanDomain.exists_pos_radius_closure_subset_ball (Omega : SmoothJordanDomain) (c : ℂ) : ∃ (R : ℝ), 0 < R ∧ closure Omega.carrier ⊆ Metric.ball c R

Around any chosen center, the closed carrier of a smooth Jordan domain is contained in a ball of some positive radius.