Differentiability of the complex log function

theorem Complex.isOpenMap_exp : IsOpenMap Complex.exp

noncomputable def Complex.expLocalHomeomorph : LocalHomeomorph ℂ ℂ

Complex.exp as a LocalHomeomorph with source = {z | -π < im z < π} and target = {z | 0 < re z} ∪ {z | im z ≠ 0}. This definition is used to prove that Complex.log is complex differentiable at all points but the negative real semi-axis.

theorem Complex.hasStrictDerivAt_log {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) : HasStrictDerivAt Complex.log x⁻¹ x

theorem Complex.hasStrictFDerivAt_log_real {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) : HasStrictFDerivAt Complex.log (x⁻¹ • 1) x

theorem Complex.contDiffAt_log {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) {n : ℕ∞} : ContDiffAt ℂ n Complex.log x

theorem HasStrictFDerivAt.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E} (h₁ : HasStrictFDerivAt f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : HasStrictFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x

theorem HasStrictDerivAt.clog {f : ℂ → ℂ} {f' : ℂ} {x : ℂ} (h₁ : HasStrictDerivAt f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : HasStrictDerivAt (fun t => Complex.log (f t)) (f' / f x) x

theorem HasStrictDerivAt.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasStrictDerivAt f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : 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' : E →L[ℂ] ℂ} {x : E} (h₁ : HasFDerivAt f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : HasFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x

theorem HasDerivAt.clog {f : ℂ → ℂ} {f' : ℂ} {x : ℂ} (h₁ : HasDerivAt f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : HasDerivAt (fun t => Complex.log (f t)) (f' / f x) x

theorem HasDerivAt.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasDerivAt f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : 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₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : DifferentiableAt ℂ (fun t => Complex.log (f t)) x

theorem HasFDerivWithinAt.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {f' : E →L[ℂ] ℂ} {s : Set E} {x : E} (h₁ : HasFDerivWithinAt f f' s x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : HasFDerivWithinAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') s x

theorem HasDerivWithinAt.clog {f : ℂ → ℂ} {f' : ℂ} {x : ℂ} {s : Set ℂ} (h₁ : HasDerivWithinAt f f' s x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : 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₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : 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₂ : 0 < (f x).re ∨ (f x).im ≠ 0) : DifferentiableWithinAt ℂ (fun t => 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 : E), x ∈ s → 0 < (f x).re ∨ (f x).im ≠ 0) : DifferentiableOn ℂ (fun t => Complex.log (f t)) s

theorem Differentiable.clog {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (h₁ : Differentiable ℂ f) (h₂ : ∀ (x : E), 0 < (f x).re ∨ (f x).im ≠ 0) : Differentiable ℂ fun t => Complex.log (f t)