Differentiability of the complex log function #

noncomputable def Complex.expPartialHomeomorph :

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.
Instances For
theorem Complex.hasDerivAt_log {z : } (hz : ) :
theorem Complex.differentiableAt_log {z : } (hz : ) :
theorem Complex.contDiffAt_log {x : } (h : ) {n : ℕ∞} :
theorem HasStrictFDerivAt.clog {E : Type u_2} [] {f : E} {f' : } {x : E} (h₁ : ) (h₂ : ) :
HasStrictFDerivAt (fun (t : E) => Complex.log (f t)) ((f x)⁻¹ f') x
theorem HasStrictDerivAt.clog {f : } {f' : } {x : } (h₁ : HasStrictDerivAt f f' x) (h₂ : ) :
HasStrictDerivAt (fun (t : ) => Complex.log (f t)) (f' / f x) x
theorem HasStrictDerivAt.clog_real {f : } {x : } {f' : } (h₁ : HasStrictDerivAt f f' x) (h₂ : ) :
HasStrictDerivAt (fun (t : ) => Complex.log (f t)) (f' / f x) x
theorem HasFDerivAt.clog {E : Type u_2} [] {f : E} {f' : } {x : E} (h₁ : HasFDerivAt f f' x) (h₂ : ) :
HasFDerivAt (fun (t : E) => Complex.log (f t)) ((f x)⁻¹ f') x
theorem HasDerivAt.clog {f : } {f' : } {x : } (h₁ : HasDerivAt f f' x) (h₂ : ) :
HasDerivAt (fun (t : ) => Complex.log (f t)) (f' / f x) x
theorem HasDerivAt.clog_real {f : } {x : } {f' : } (h₁ : HasDerivAt f f' x) (h₂ : ) :
HasDerivAt (fun (t : ) => Complex.log (f t)) (f' / f x) x
theorem DifferentiableAt.clog {E : Type u_2} [] {f : E} {x : E} (h₁ : ) (h₂ : ) :
DifferentiableAt (fun (t : E) => Complex.log (f t)) x
theorem HasFDerivWithinAt.clog {E : Type u_2} [] {f : E} {f' : } {s : Set E} {x : E} (h₁ : HasFDerivWithinAt f f' s x) (h₂ : ) :
HasFDerivWithinAt (fun (t : E) => Complex.log (f t)) ((f x)⁻¹ f') s x
theorem HasDerivWithinAt.clog {f : } {f' : } {x : } {s : } (h₁ : HasDerivWithinAt f f' s x) (h₂ : ) :
HasDerivWithinAt (fun (t : ) => Complex.log (f t)) (f' / f x) s x
theorem HasDerivWithinAt.clog_real {f : } {s : } {x : } {f' : } (h₁ : HasDerivWithinAt f f' s x) (h₂ : ) :
HasDerivWithinAt (fun (t : ) => Complex.log (f t)) (f' / f x) s x
theorem DifferentiableWithinAt.clog {E : Type u_2} [] {f : E} {s : Set E} {x : E} (h₁ : ) (h₂ : ) :
DifferentiableWithinAt (fun (t : E) => Complex.log (f t)) s x
theorem DifferentiableOn.clog {E : Type u_2} [] {f : E} {s : Set E} (h₁ : ) (h₂ : xs, ) :
DifferentiableOn (fun (t : E) => Complex.log (f t)) s
theorem Differentiable.clog {E : Type u_2} [] {f : E} (h₁ : ) (h₂ : ∀ (x : E), ) :
Differentiable fun (t : E) => Complex.log (f t)
theorem Complex.deriv_log_comp_eq_logDeriv {f : } {x : } (h₁ : ) (h₂ : ) :

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