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
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 : ℕ∞}
:
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.