Differentiability of the complex log
function #
Complex.exp
as a LocalHomeomorph
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.
Instances For
theorem
Complex.hasStrictFDerivAt_log_real
{x : ℂ}
(h : 0 < x.re ∨ x.im ≠ 0)
:
HasStrictFDerivAt Complex.log (x⁻¹ • 1) x
theorem
Complex.contDiffAt_log
{x : ℂ}
(h : 0 < x.re ∨ x.im ≠ 0)
{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₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
HasStrictFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x
theorem
HasStrictDerivAt.clog
{f : ℂ → ℂ}
{f' : ℂ}
{x : ℂ}
(h₁ : HasStrictDerivAt f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
HasStrictDerivAt (fun t => Complex.log (f t)) (f' / f x) x
theorem
HasStrictDerivAt.clog_real
{f : ℝ → ℂ}
{x : ℝ}
{f' : ℂ}
(h₁ : HasStrictDerivAt f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
HasFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x
theorem
HasDerivAt.clog
{f : ℂ → ℂ}
{f' : ℂ}
{x : ℂ}
(h₁ : HasDerivAt f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
HasDerivAt (fun t => Complex.log (f t)) (f' / f x) x
theorem
HasDerivAt.clog_real
{f : ℝ → ℂ}
{x : ℝ}
{f' : ℂ}
(h₁ : HasDerivAt f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
DifferentiableAt ℂ (fun t => 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₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
HasFDerivWithinAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') s x
theorem
HasDerivWithinAt.clog
{f : ℂ → ℂ}
{f' : ℂ}
{x : ℂ}
{s : Set ℂ}
(h₁ : HasDerivWithinAt f f' s x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
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₂ : 0 < (f x).re ∨ (f x).im ≠ 0)
:
DifferentiableWithinAt ℂ (fun t => 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 : E), x ∈ s → 0 < (f x).re ∨ (f x).im ≠ 0)
:
DifferentiableOn ℂ (fun t => Complex.log (f t)) s
theorem
Differentiable.clog
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : E → ℂ}
(h₁ : Differentiable ℂ f)
(h₂ : ∀ (x : E), 0 < (f x).re ∨ (f x).im ≠ 0)
:
Differentiable ℂ fun t => Complex.log (f t)