Documentation

Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Differentiability of the complex log function #

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 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₂ : xs, 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)

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