Documentation

Mathlib.Analysis.Calculus.LogDeriv

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
Instances For
    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