Entire logarithms for zero-free entire functions

This file provides a basic construction: if f : ℂ → ℂ is complex-differentiable everywhere and never vanishes, then there exists a complex-differentiable function g with f = exp ∘ g.

We use:

• Complex.isCoveringMap_exp to lift f (viewed as a map into ℂˣ) through exp;
• a local inverse of exp (inverse function theorem) to upgrade the lift from continuous to complex-differentiable.

theorem EntireLog.entire_has_entire_log_of_no_zeros (f : ℂ → ℂ) (hf : Differentiable ℂ f) (h0 : ∀ (z : ℂ), f z ≠ 0) : ∃ (g : ℂ → ℂ), Differentiable ℂ g ∧ ∀ (z : ℂ), f z = Complex.exp (g z)