Holomorphic Primitives on Convex Sets

Construction of a primitive F for a holomorphic function f on a convex open set S via the segment integral F(z) = ∫₀¹ f(c + t(z-c))·(z-c) dt.

Main Results

• holomorphic_convex_primitive — holomorphic on convex open ⇒ has primitive

theorem holomorphic_convex_primitive {f : ℂ → ℂ} {S : Set ℂ} (hS_convex : Convex ℝ S) (hS_open : IsOpen S) (hS_ne : S.Nonempty) (hf : DifferentiableOn ℂ f S) : ∃ (F : ℂ → ℂ), ∀ z ∈ S, HasDerivAt F (f z) z

For a convex open set, holomorphic functions have primitives.

Construction: For f holomorphic on convex open S and c ∈ S, F(z) = ∫₀¹ f(c + t(z-c))·(z-c) dt is a primitive with F'(z) = f(z).