Frontiers of local half-planes and sectors

When a domain agrees locally with an open half-plane, its frontier lies on the bounding line. When it agrees locally with an open sector, its frontier away from the vertex lies on the bounding rays, and the vertex itself lies on the frontier. When it agrees far out with an open sector of opening less than 2π, some point lies outside its closure. When it agrees far out with an open half-strip, its frontier far out lies on the two bounding rays, and again some point lies outside its closure. These facts supply the boundary conditions for polygonal conformal maps.

theorem TauCeti.continuousAt_abs_arg {w : ℂ} (hw : w ≠ 0) : ContinuousAt (fun (z : ℂ) => |z.arg|) w

The absolute value of the argument, the unoriented angle with 1, is continuous away from 0, across the negative real axis too, where the argument itself jumps.

The frontier near a side and near a vertex

theorem TauCeti.im_div_eq_zero_of_mem_frontier {U : Set ℂ} {w q b z : ℂ} {ρ : ℝ} (hU : ∀ y ∈ Metric.ball w ρ, y ∈ U ↔ 0 < ((y - q) / b).im) (hz : z ∈ Metric.ball w ρ) (hzU : z ∈ frontier U) : ((z - q) / b).im = 0

Near a boundary point where U coincides with an open half-plane, the frontier of U lies on the bounding line.

theorem TauCeti.abs_arg_div_eq_of_mem_frontier {U V : Set ℂ} {v b z : ℂ} {α : ℝ} (hb : b ≠ 0) (hV : IsOpen V) (hU : ∀ y ∈ V, y ≠ v → (y ∈ U ↔ |((y - v) / b).arg| < α)) (hz : z ∈ V) (hzv : z ≠ v) (hzU : z ∈ frontier U) : |((z - v) / b).arg| = α

On an open set V where U coincides, away from the vertex v, with the open sector {|arg ((z - v) / b)| < α}, the frontier of U away from the vertex lies on the two bounding rays |arg ((z - v) / b)| = α. Typically V is a ball about the vertex, or the exterior of a ball when U is a sector near infinity.

theorem TauCeti.mem_frontier_of_forall_mem_iff_abs_arg_lt {U : Set ℂ} {v b : ℂ} {ρ α : ℝ} (hρ : 0 < ρ) (hb : b ≠ 0) (hα₀ : 0 < α) (hα : α ≤ Real.pi) (hU : ∀ z ∈ Metric.ball v ρ, z ≠ v → (z ∈ U ↔ |((z - v) / b).arg| < α)) : v ∈ frontier U

If a set U coincides near v, away from v itself, with the open sector {|arg ((z - v) / b)| < α} of half-opening α ∈ (0, π], then the vertex v lies on the frontier of U.

A sector at infinity

theorem TauCeti.exists_notMem_closure_of_forall_mem_iff_abs_arg_lt {U : Set ℂ} {c b : ℂ} {ρ α : ℝ} (hb : b ≠ 0) (hα : α < Real.pi) (hU : ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ |((z - c) / b).arg| < α)) : ∃ (q : ℂ), q ∉ closure U

If a set U coincides far from c with the open sector {|arg ((z - c) / b)| < α} of half-opening α < π, then some point lies outside the closure of U, far out on the ray opposite to the sector.

A half-strip at infinity

theorem TauCeti.re_div_nonneg_and_im_div_eq_zero_or_eq_pi_of_mem_frontier {U : Set ℂ} {c b z : ℂ} {ρ : ℝ} (hU : ∀ (y : ℂ), ρ < ‖y - c‖ → (y ∈ U ↔ 0 < ((y - c) / b).re ∧ ((y - c) / b).im ∈ Set.Ioo 0 Real.pi)) (hzρ : ρ < ‖z - c‖) (hzb : Real.pi * ‖b‖ < ‖z - c‖) (hzU : z ∈ frontier U) : 0 ≤ ((z - c) / b).re ∧ (((z - c) / b).im = 0 ∨ ((z - c) / b).im = Real.pi)

If a set U coincides far from c with the open half-strip {0 < re ((z - c) / b), 0 < im ((z - c) / b) < π}, then far from c the frontier of U lies on the two bounding rays im ((z - c) / b) ∈ {0, π}, with 0 ≤ re ((z - c) / b). Here "far" also excludes the short side re ((z - c) / b) = 0 of the half-strip, which lies within distance π * ‖b‖ of c.

theorem TauCeti.exists_notMem_closure_of_forall_mem_re_div_pos {U : Set ℂ} {c b : ℂ} {ρ : ℝ} (hb : b ≠ 0) (hU : ∀ (z : ℂ), ρ < ‖z - c‖ → z ∈ U → 0 < ((z - c) / b).re) : ∃ (q : ℂ), q ∉ closure U

If, far from c, every point z of a set U has 0 < re ((z - c) / b) (as for a set that coincides far out with a half-strip or a half-plane), then some point lies outside the closure of U, far out in the direction -b.