Continuity of arg and log on the closed upper half-plane

The principal argument and logarithm are continuous on the punctured closed upper half-plane {z | 0 ≤ im z ∧ z ≠ 0}. This strengthens Mathlib's continuity on the open slit plane: the negative real axis is allowed because the approach is confined to nonnegative imaginary parts, where arg agrees with the continuous arccos formula. It is the boundary-tolerant ingredient for logarithmic primitives along contours that touch the slit-plane boundary.

Main declarations

• TauCeti.continuousOn_arg_im_nonneg_ne_zero.
• TauCeti.continuousOn_log_im_nonneg_ne_zero.
• TauCeti.continuousOn_cpow_const_im_nonneg.

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/WindingWeights/Common.lean) this file ports onto the current Mathlib pin.

theorem TauCeti.continuousOn_arg_im_nonneg_ne_zero : ContinuousOn Complex.arg {z : ℂ | 0 ≤ z.im ∧ z ≠ 0}

The principal argument is continuous on the punctured closed upper half-plane: the approach is confined to nonnegative imaginary parts, where arg is the arccos of the normalized real part.

theorem TauCeti.continuousOn_log_im_nonneg_ne_zero : ContinuousOn Complex.log {z : ℂ | 0 ≤ z.im ∧ z ≠ 0}

The principal logarithm is continuous on the punctured closed upper half-plane.

theorem TauCeti.continuousOn_cpow_const_im_nonneg {r : ℂ} (hr : 0 < r.re) : ContinuousOn (fun (z : ℂ) => z ^ r) {z : ℂ | 0 ≤ z.im}

A complex power whose exponent has positive real part is continuous on the closed upper half-plane. Unlike continuity on the open slit plane, this includes one-sided continuity at the negative real axis; positivity of the exponent's real part also supplies continuity at zero.