mathlib3 documentation

analysis.special_functions.complex.log_deriv

Differentiability of the complex log function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

complex.exp as a local_homeomorph 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
theorem complex.cont_diff_at_log {x : } (h : 0 < x.re x.im 0) {n : ℕ∞} :
theorem has_strict_fderiv_at.clog {E : Type u_2} [normed_add_comm_group E] [normed_space E] {f : E } {f' : E →L[] } {x : E} (h₁ : has_strict_fderiv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_strict_fderiv_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ f') x
theorem has_strict_deriv_at.clog {f : } {f' x : } (h₁ : has_strict_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_strict_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem has_strict_deriv_at.clog_real {f : } {x : } {f' : } (h₁ : has_strict_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_strict_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem has_fderiv_at.clog {E : Type u_2} [normed_add_comm_group E] [normed_space E] {f : E } {f' : E →L[] } {x : E} (h₁ : has_fderiv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_fderiv_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ f') x
theorem has_deriv_at.clog {f : } {f' x : } (h₁ : has_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem has_deriv_at.clog_real {f : } {x : } {f' : } (h₁ : has_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem differentiable_at.clog {E : Type u_2} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (h₁ : differentiable_at f x) (h₂ : 0 < (f x).re (f x).im 0) :
differentiable_at (λ (t : E), complex.log (f t)) x
theorem has_fderiv_within_at.clog {E : Type u_2} [normed_add_comm_group E] [normed_space E] {f : E } {f' : E →L[] } {s : set E} {x : E} (h₁ : has_fderiv_within_at f f' s x) (h₂ : 0 < (f x).re (f x).im 0) :
has_fderiv_within_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ f') s x
theorem has_deriv_within_at.clog {f : } {f' x : } {s : set } (h₁ : has_deriv_within_at f f' s x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_within_at (λ (t : ), complex.log (f t)) (f' / f x) s x
theorem has_deriv_within_at.clog_real {f : } {s : set } {x : } {f' : } (h₁ : has_deriv_within_at f f' s x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_within_at (λ (t : ), complex.log (f t)) (f' / f x) s x
theorem differentiable_within_at.clog {E : Type u_2} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} {x : E} (h₁ : differentiable_within_at f s x) (h₂ : 0 < (f x).re (f x).im 0) :
differentiable_within_at (λ (t : E), complex.log (f t)) s x
theorem differentiable_on.clog {E : Type u_2} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (h₁ : differentiable_on f s) (h₂ : (x : E), x s 0 < (f x).re (f x).im 0) :
differentiable_on (λ (t : E), complex.log (f t)) s
theorem differentiable.clog {E : Type u_2} [normed_add_comm_group E] [normed_space E] {f : E } (h₁ : differentiable f) (h₂ : (x : E), 0 < (f x).re (f x).im 0) :
differentiable (λ (t : E), complex.log (f t))