Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Log

The complex log function #

Basic properties, relationship with exp.

noncomputable def Complex.log (x : ) :

Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π. log 0 = 0

Equations
Instances For
    theorem Complex.log_re (x : ) :
    (Complex.log x).re = Real.log (Complex.abs x)
    theorem Complex.log_im (x : ) :
    (Complex.log x).im = x.arg
    theorem Complex.exp_log {x : } (hx : x 0) :
    theorem Complex.log_exp {x : } (hx₁ : -Real.pi < x.im) (hx₂ : x.im Real.pi) :
    theorem Complex.exp_inj_of_neg_pi_lt_of_le_pi {x : } {y : } (hx₁ : -Real.pi < x.im) (hx₂ : x.im Real.pi) (hy₁ : -Real.pi < y.im) (hy₂ : y.im Real.pi) (hxy : Complex.exp x = Complex.exp y) :
    x = y
    theorem Complex.ofReal_log {x : } (hx : 0 x) :
    (Real.log x) = Complex.log x
    @[simp]
    theorem Complex.natCast_log {n : } :
    (Real.log n) = Complex.log n
    @[simp]
    theorem Complex.ofNat_log {n : } [n.AtLeastTwo] :
    theorem Complex.log_ofReal_mul {r : } (hr : 0 < r) {x : } (hx : x 0) :
    Complex.log (r * x) = (Real.log r) + Complex.log x
    theorem Complex.log_mul_ofReal (r : ) (hr : 0 < r) (x : ) (hx : x 0) :
    Complex.log (x * r) = (Real.log r) + Complex.log x
    theorem Complex.log_mul_eq_add_log_iff {x : } {y : } (hx₀ : x 0) (hy₀ : y 0) :
    theorem Complex.log_mul {x : } {y : } (hx₀ : x 0) (hy₀ : y 0) :

    Alias of the reverse direction of Complex.log_mul_eq_add_log_iff.

    @[simp]
    @[simp]
    theorem Complex.exp_eq_one_iff {x : } :
    Complex.exp x = 1 ∃ (n : ), x = n * (2 * Real.pi * Complex.I)
    theorem Complex.exp_eq_exp_iff_exists_int {x : } {y : } :
    Complex.exp x = Complex.exp y ∃ (n : ), x = y + n * (2 * Real.pi * Complex.I)
    @[simp]
    theorem Complex.countable_preimage_exp {s : Set } :
    (Complex.exp ⁻¹' s).Countable s.Countable
    theorem Set.Countable.preimage_cexp {s : Set } :
    s.Countable(Complex.exp ⁻¹' s).Countable

    Alias of the reverse direction of Complex.countable_preimage_exp.

    theorem Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
    Filter.Tendsto Complex.log (nhdsWithin z {z : | z.im < 0}) (nhds ((Real.log (Complex.abs z)) - Real.pi * Complex.I))
    theorem Complex.continuousWithinAt_log_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
    theorem Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
    Filter.Tendsto Complex.log (nhdsWithin z {z : | 0 z.im}) (nhds ((Real.log (Complex.abs z)) + Real.pi * Complex.I))
    theorem Filter.Tendsto.clog {α : Type u_1} {l : Filter α} {f : α} {x : } (h : Filter.Tendsto f l (nhds x)) (hx : x Complex.slitPlane) :
    Filter.Tendsto (fun (t : α) => Complex.log (f t)) l (nhds (Complex.log x))
    theorem ContinuousAt.clog {α : Type u_1} [TopologicalSpace α] {f : α} {x : α} (h₁ : ContinuousAt f x) (h₂ : f x Complex.slitPlane) :
    ContinuousAt (fun (t : α) => Complex.log (f t)) x
    theorem ContinuousWithinAt.clog {α : Type u_1} [TopologicalSpace α] {f : α} {s : Set α} {x : α} (h₁ : ContinuousWithinAt f s x) (h₂ : f x Complex.slitPlane) :
    ContinuousWithinAt (fun (t : α) => Complex.log (f t)) s x
    theorem ContinuousOn.clog {α : Type u_1} [TopologicalSpace α] {f : α} {s : Set α} (h₁ : ContinuousOn f s) (h₂ : xs, f x Complex.slitPlane) :
    ContinuousOn (fun (t : α) => Complex.log (f t)) s
    theorem Continuous.clog {α : Type u_1} [TopologicalSpace α] {f : α} (h₁ : Continuous f) (h₂ : ∀ (x : α), f x Complex.slitPlane) :
    Continuous fun (t : α) => Complex.log (f t)
    theorem Real.HasSum_rexp_HasProd {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), 0 < f n x) (hf : ∀ (x : α), HasSum (fun (n : ι) => Real.log (f n x)) (∑' (i : ι), Real.log (f i x))) (a : α) :
    HasProd (fun (b : ι) => f b a) (∏' (n : ι), f n a)
    theorem Real.rexp_tsum_eq_tprod {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), 0 < f n x) (hf : ∀ (x : α), Summable fun (n : ι) => Real.log (f n x)) :
    (Real.exp fun (a : α) => ∑' (n : ι), Real.log (f n a)) = fun (a : α) => ∏' (n : ι), f n a

    The exponential of a infinite sum of real logs (which converges absolutely) is an infinite product.

    theorem Real.summable_cexp_multipliable {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), 0 < f n x) (hf : ∀ (x : α), Summable fun (n : ι) => Real.log (f n x)) (a : α) :
    Multipliable fun (b : ι) => f b a
    theorem Complex.HasSum_cexp_HasProd {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), f n x 0) (hf : ∀ (x : α), HasSum (fun (n : ι) => Complex.log (f n x)) (∑' (i : ι), Complex.log (f i x))) (a : α) :
    HasProd (fun (b : ι) => f b a) (∏' (n : ι), f n a)
    theorem Complex.summable_cexp_multipliable {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), f n x 0) (hf : ∀ (x : α), Summable fun (n : ι) => Complex.log (f n x)) (a : α) :
    Multipliable fun (b : ι) => f b a
    theorem Complex.cexp_tsum_eq_tprod {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), f n x 0) (hf : ∀ (x : α), Summable fun (n : ι) => Complex.log (f n x)) :
    (Complex.exp fun (a : α) => ∑' (n : ι), Complex.log (f n a)) = fun (a : α) => ∏' (n : ι), f n a

    The exponential of a infinite sum of comples logs (which converges absolutely) is an infinite product.