Logs of nonzero analytic functions

Stream: Is there code for X?

[Geoffrey Irving]

I need

lemma AnalyticOnNhd.exists_clog {f : ℂ → ℂ} (fa : AnalyticOnNhd ℂ f (ball 0 1))
    (f0 : ∀ z ∈ ball 0 1, f z ≠ 0) :
    ∃ g : ℂ → ℂ, AnalyticOnNhd ℂ g (ball 0 1) ∧ ∀ z ∈ ball 0 1, f z = Complex.exp (g z) := by
  sorry

I can prove this via my analytic continuation machinery in https://github.com/girving/ray/blob/main/Ray/Misc/Continuation.lean, but possibly it exists already?

[Junyan Xu]

You may take the primitive of df/f using #9598, or use IsCoveringMap.existsUnique_continuousMap_lifts (I have proven exp is a covering map (not yet PR'd), but you have to show the lifted map is analytic).

[Geoffrey Irving]

https://github.com/girving/ray/blob/main/Ray/Analytic/Log.lean#L33