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
- complex.exp_local_homeomorph = local_homeomorph.of_continuous_open {to_fun := complex.exp, inv_fun := complex.log, source := {z : ℂ | z.im ∈ set.Ioo (-real.pi) real.pi}, target := {z : ℂ | 0 < z.re} ∪ {z : ℂ | z.im ≠ 0}, map_source' := complex.exp_local_homeomorph._proof_1, map_target' := complex.exp_local_homeomorph._proof_2, left_inv' := complex.exp_local_homeomorph._proof_3, right_inv' := complex.exp_local_homeomorph._proof_4} complex.exp_local_homeomorph._proof_5 complex.is_open_map_exp complex.exp_local_homeomorph._proof_6
theorem
complex.has_strict_fderiv_at_log_real
{x : ℂ}
(h : 0 < x.re ∨ x.im ≠ 0) :
has_strict_fderiv_at complex.log (x⁻¹ • 1) x
theorem
complex.cont_diff_at_log
{x : ℂ}
(h : 0 < x.re ∨ x.im ≠ 0)
{n : ℕ∞} :
cont_diff_at ℂ n complex.log x
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))