Differentiability of the complex log function

theorem Complex.isOpenMap_exp : IsOpenMap Complex.exp

noncomputable def Complex.expPartialHomeomorph : PartialHomeomorph ℂ ℂ

Complex.exp as a PartialHomeomorph 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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

theorem Complex.contDiffAt_log {x : ℂ} (h : x ∈ Complex.slitPlane) {n : WithTop ℕ∞} : 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₂ : 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' : E →L[ℂ] ℂ} {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' : E →L[ℂ] ℂ} {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 ∈ Complex.slitPlane) : deriv (Complex.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.