has primitive implies holomorphic

Stream: Is there code for X?

[Alex Kontorovich]

What's an easy way to go from F being a primitive of f to f being holomorphic?

import Mathlib

example {f F : ℂ → ℂ} {U : Set ℂ} (U_open : IsOpen U) (F_prim : ∀ z ∈ U, HasDerivAt F (f z) z)
    {z : ℂ} (hz : z ∈ U):
    DifferentiableAt ℂ f z := by
  have F_differentiableOn : DifferentiableOn ℂ F U := fun z hz ↦
   (F_prim z hz).differentiableAt.differentiableWithinAt
  have := DifferentiableOn.contDiffOn (hd := F_differentiableOn) (hs := U_open) (n := 2) z hz
  -- this : ContDiffWithinAt ℂ 2 F U z

[Junyan Xu]

One solution:

import Mathlib

example {f F : ℂ → ℂ} {U : Set ℂ} (U_open : IsOpen U) (F_prim : ∀ z ∈ U, HasDerivAt F (f z) z)
    {z : ℂ} (hz : z ∈ U):
    DifferentiableAt ℂ f z := by
  have : AnalyticOn ℂ F U := DifferentiableOn.analyticOn
    (fun z hz ↦ ⟨_, (F_prim z hz).hasDerivWithinAt⟩) U_open
  refine (AnalyticOn.differentiableOn ?_).differentiableAt (U_open.mem_nhds hz)
  exact this.deriv.congr U_open fun z hz ↦ (F_prim z hz).deriv