7.7. Path.Primitive🔗

Jacobians.Path.Primitive — source

exists_primitive_of_convex

Holomorphic functions on a convex open set have a primitive. If h is complex- differentiable on a convex open U ⊆ ℂ, there is F with HasDerivAt F (h z) z for every z ∈ U.

theorem exists_primitive_of_convex {U : Set ℂ} (hU : Convex ℝ U) (hUo : IsOpen U)
    {h : ℂ → ℂ} (hh : DifferentiableOn ℂ h U) :
    ∃ F : ℂ → ℂ, ∀ z ∈ U, HasDerivAt F (h z) z