Injectivity from a half-plane constraint on the derivative

A complex function on a convex set is injective if a fixed rotation of its derivative has strictly positive real part. This gives an analytic univalence criterion that does not require control of the boundary curve. Along the segment between two points, the real part of the rotated difference quotient is strictly increasing.

The criterion is commonly called the Noshiro--Warschawski criterion. Here the derivative condition itself implies differentiability, so the domain need not be open.

theorem TauCeti.injOn_of_re_mul_deriv_pos {U : Set ℂ} (hU : Convex ℝ U) {f : ℂ → ℂ} (c : ℂ) (hf : ∀ z ∈ U, 0 < (c * deriv f z).re) : Set.InjOn f U

A complex function on a convex set is injective if a fixed complex multiple of its derivative has strictly positive real part throughout the set.