Geometry of the complex slit plane

The quotient z₂ / z₁ of two points of an open half-plane through the origin is never a nonpositive real, so it lies in Complex.slitPlane. The half-plane is encoded by a normal direction a: its members are the z with 0 < (conj a * z).re. Specializations to the four axis-aligned half-planes cover the common cases.

The module also records a locally uniform lower bound for the distance from a point of the slit plane to the closed negative half-axis. This bound locally dominates slit-plane kernels and thus supports differentiation and holomorphy arguments for parameter-dependent Stieltjes integrals.

These criteria feed logarithm evaluations of index integrals: a curve piece confined to a half-plane about the winding point has slit-compatible chord ratios, so its index integral is a principal logarithm.

Main declarations

• TauCeti.div_mem_slitPlane_of_re_conj_mul_pos
• TauCeti.div_mem_slitPlane_of_re_pos, …_of_re_neg, …_of_im_pos, …_of_im_neg
• TauCeti.exists_pos_forall_mem_ball_mul_one_add_le_norm_add

theorem TauCeti.div_mem_slitPlane_of_re_conj_mul_pos {a z₁ z₂ : ℂ} (h₁ : 0 < ((starRingEnd ℂ) a * z₁).re) (h₂ : 0 < ((starRingEnd ℂ) a * z₂).re) : z₂ / z₁ ∈ Complex.slitPlane

The ratio of two members of an open half-plane through the origin lies in the slit plane. The half-plane with normal direction a is {z | 0 < (conj a * z).re}; degenerate a admits no members, so no nonvanishing hypothesis is needed.

theorem TauCeti.div_mem_slitPlane_of_re_pos {z₁ z₂ : ℂ} (h₁ : 0 < z₁.re) (h₂ : 0 < z₂.re) : z₂ / z₁ ∈ Complex.slitPlane

Two points in the right half-plane have their ratio in the slit plane.

theorem TauCeti.div_mem_slitPlane_of_re_neg {z₁ z₂ : ℂ} (h₁ : z₁.re < 0) (h₂ : z₂.re < 0) : z₂ / z₁ ∈ Complex.slitPlane

Two points in the left half-plane have their ratio in the slit plane.

theorem TauCeti.div_mem_slitPlane_of_im_pos {z₁ z₂ : ℂ} (h₁ : 0 < z₁.im) (h₂ : 0 < z₂.im) : z₂ / z₁ ∈ Complex.slitPlane

Two points in the upper half-plane have their ratio in the slit plane.

theorem TauCeti.div_mem_slitPlane_of_im_neg {z₁ z₂ : ℂ} (h₁ : z₁.im < 0) (h₂ : z₂.im < 0) : z₂ / z₁ ∈ Complex.slitPlane

Two points in the lower half-plane have their ratio in the slit plane.

theorem TauCeti.exists_pos_forall_mem_ball_mul_one_add_le_norm_add {z : ℂ} (hz : z ∈ Complex.slitPlane) : ∃ c > 0, ∀ w ∈ Metric.ball z c, ∀ (x : NNReal), c * (1 + ↑x) ≤ ‖w + ↑↑x‖

On a small ball around a point of the slit plane, the distance from w to the point -x of the closed negative half-axis is bounded below by a fixed multiple of 1 + x.