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.

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_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