Logarithmic Derivatives

We define the logarithmic derivative of a function f as deriv f / f. We then prove some basic facts about this, including how it changes under multiplication and composition.

noncomputable def logDeriv {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜') (x : 𝕜) : 𝕜'

The logarithmic derivative of a function defined as deriv f /f. Note that it will be zero at x if f is not DifferentiableAt x.

Equations

• logDeriv f = deriv f / f

theorem logDeriv_apply {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜') (x : 𝕜) : logDeriv f x = deriv f x / f x

theorem logDeriv_eq_zero_of_not_differentiableAt {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜') (x : 𝕜) (h : ¬DifferentiableAt 𝕜 f x) : logDeriv f x = 0

@[simp]

theorem logDeriv_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) : logDeriv id x = 1 / x

@[simp]

theorem logDeriv_id' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) : logDeriv (fun (x : 𝕜) => x) x = 1 / x

@[simp]

theorem logDeriv_const {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] (a : 𝕜') : (logDeriv fun (x : 𝕜) => a) = 0

theorem logDeriv_mul {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} (x : 𝕜) (hf : f x ≠ 0) (hg : g x ≠ 0) (hdf : DifferentiableAt 𝕜 f x) (hdg : DifferentiableAt 𝕜 g x) : logDeriv (fun (z : 𝕜) => f z * g z) x = logDeriv f x + logDeriv g x

theorem logDeriv_div {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} (x : 𝕜) (hf : f x ≠ 0) (hg : g x ≠ 0) (hdf : DifferentiableAt 𝕜 f x) (hdg : DifferentiableAt 𝕜 g x) : logDeriv (fun (z : 𝕜) => f z / g z) x = logDeriv f x - logDeriv g x

theorem logDeriv_mul_const {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜') (ha : a ≠ 0) : logDeriv (fun (z : 𝕜) => f z * a) x = logDeriv f x

theorem logDeriv_const_mul {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜') (ha : a ≠ 0) : logDeriv (fun (z : 𝕜) => a * f z) x = logDeriv f x

theorem logDeriv_prod {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜'} {x : 𝕜} (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) : logDeriv (fun (x : 𝕜) => ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x

The logarithmic derivative of a finite product is the sum of the logarithmic derivatives.

theorem logDeriv_fun_zpow {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜} (hdf : DifferentiableAt 𝕜 f x) (n : ℤ) : logDeriv (fun (x : 𝕜) => f x ^ n) x = ↑n * logDeriv f x

theorem logDeriv_fun_pow {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜} (hdf : DifferentiableAt 𝕜 f x) (n : ℕ) : logDeriv (fun (x : 𝕜) => f x ^ n) x = ↑n * logDeriv f x

@[simp]

theorem logDeriv_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) (n : ℤ) : logDeriv (fun (x : 𝕜) => x ^ n) x = ↑n / x

@[simp]

theorem logDeriv_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) (n : ℕ) : logDeriv (fun (x : 𝕜) => x ^ n) x = ↑n / x

@[simp]

theorem logDeriv_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) : logDeriv (fun (x : 𝕜) => x⁻¹) x = -1 / x

theorem logDeriv_comp {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜' → 𝕜'} {g : 𝕜 → 𝕜'} {x : 𝕜} (hf : DifferentiableAt 𝕜' f (g x)) (hg : DifferentiableAt 𝕜 g x) : logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x

theorem logDeriv_eqOn_iff {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [IsRCLikeNormedField 𝕜] {f g : 𝕜 → 𝕜'} {s : Set 𝕜} (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hs2 : IsOpen s) (hsc : IsPreconnected s) (hgn : ∀ x ∈ s, g x ≠ 0) (hfn : ∀ x ∈ s, f x ≠ 0) : Set.EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ Set.EqOn f (z • g) s

theorem AnalyticAt.tendsto_mul_logDeriv_simple_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) (hfx : f x = 0) (hf' : deriv f x ≠ 0) : Filter.Tendsto (fun (w : 𝕜) => (w - x) * logDeriv f w) (nhdsWithin x {x}ᶜ) (nhds 1)

At a simple zero of an analytic function, the logarithmic residue (w - x) * logDeriv f w tends to 1.