Differentiability of the complex log function

theorem Complex.isOpenMap_exp : IsOpenMap exp

theorem Complex.hasStrictDerivAt_log {x : ℂ} (h : x ∈ slitPlane) : HasStrictDerivAt log x⁻¹ x

theorem Complex.hasDerivAt_log {z : ℂ} (hz : z ∈ slitPlane) : HasDerivAt log z⁻¹ z

theorem Complex.differentiableAt_log {z : ℂ} (hz : z ∈ slitPlane) : DifferentiableAt ℂ log z

theorem Complex.hasStrictFDerivAt_log_real {x : ℂ} (h : x ∈ slitPlane) : HasStrictFDerivAt log (x⁻¹ • 1) x

theorem Complex.contDiffAt_log {x : ℂ} (h : x ∈ slitPlane) {n : WithTop ℕ∞} : ContDiffAt ℂ n log x

theorem HasStrictFDerivAt.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E} (h₁ : HasStrictFDerivAt f f' x) (h₂ : f x ∈ Complex.slitPlane) : HasStrictFDerivAt (fun (t : E) => Complex.log (f t)) ((f x)⁻¹ • f') x

theorem HasStrictDerivAt.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : HasStrictDerivAt f f' x) (h₂ : f x ∈ Complex.slitPlane) : HasStrictDerivAt (fun (t : ℂ) => Complex.log (f t)) (f' / f x) x

theorem HasStrictDerivAt.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasStrictDerivAt f f' x) (h₂ : f x ∈ Complex.slitPlane) : HasStrictDerivAt (fun (t : ℝ) => Complex.log (f t)) (f' / f x) x

theorem HasFDerivAt.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E} (h₁ : HasFDerivAt f f' x) (h₂ : f x ∈ Complex.slitPlane) : HasFDerivAt (fun (t : E) => Complex.log (f t)) ((f x)⁻¹ • f') x

theorem HasDerivAt.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : HasDerivAt f f' x) (h₂ : f x ∈ Complex.slitPlane) : HasDerivAt (fun (t : ℂ) => Complex.log (f t)) (f' / f x) x

theorem HasDerivAt.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasDerivAt f f' x) (h₂ : f x ∈ Complex.slitPlane) : HasDerivAt (fun (t : ℝ) => Complex.log (f t)) (f' / f x) x

theorem DifferentiableAt.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (h₁ : DifferentiableAt ℂ f x) (h₂ : f x ∈ Complex.slitPlane) : DifferentiableAt ℂ (fun (t : E) => Complex.log (f t)) x

theorem HasFDerivWithinAt.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {s : Set E} {x : E} (h₁ : HasFDerivWithinAt f f' s x) (h₂ : f x ∈ Complex.slitPlane) : HasFDerivWithinAt (fun (t : E) => Complex.log (f t)) ((f x)⁻¹ • f') s x

theorem HasDerivWithinAt.clog {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ} (h₁ : HasDerivWithinAt f f' s x) (h₂ : f x ∈ Complex.slitPlane) : HasDerivWithinAt (fun (t : ℂ) => Complex.log (f t)) (f' / f x) s x

theorem HasDerivWithinAt.clog_real {f : ℝ → ℂ} {s : Set ℝ} {x : ℝ} {f' : ℂ} (h₁ : HasDerivWithinAt f f' s x) (h₂ : f x ∈ Complex.slitPlane) : HasDerivWithinAt (fun (t : ℝ) => Complex.log (f t)) (f' / f x) s x

theorem DifferentiableWithinAt.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {x : E} (h₁ : DifferentiableWithinAt ℂ f s x) (h₂ : f x ∈ Complex.slitPlane) : DifferentiableWithinAt ℂ (fun (t : E) => Complex.log (f t)) s x

theorem DifferentiableOn.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} (h₁ : DifferentiableOn ℂ f s) (h₂ : ∀ x ∈ s, f x ∈ Complex.slitPlane) : DifferentiableOn ℂ (fun (t : E) => Complex.log (f t)) s

theorem Differentiable.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (h₁ : Differentiable ℂ f) (h₂ : ∀ (x : E), f x ∈ Complex.slitPlane) : Differentiable ℂ fun (t : E) => Complex.log (f t)

theorem Complex.deriv_log_comp_eq_logDeriv {f : ℂ → ℂ} {x : ℂ} (h₁ : DifferentiableAt ℂ f x) (h₂ : f x ∈ slitPlane) : deriv (log ∘ f) x = logDeriv f x

The derivative of log ∘ f is the logarithmic derivative provided f is differentiable and we are on the slitPlane.

theorem MeromorphicOn.logDeriv {𝕜 : Type u_3} {𝕜' : Type u_4} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {f : 𝕜 → 𝕜'} {s : Set 𝕜} (h : MeromorphicOn f s) : MeromorphicOn (logDeriv f) s

theorem Meromorphic.logDeriv {𝕜 : Type u_3} {𝕜' : Type u_4} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {f : 𝕜 → 𝕜'} (h : Meromorphic f) : Meromorphic (logDeriv f)