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
.
Instances For
theorem
logDeriv_apply
{๐ : Type u_1}
{๐' : Type u_2}
[NontriviallyNormedField ๐]
[NontriviallyNormedField ๐']
[NormedAlgebra ๐ ๐']
(f : ๐ โ ๐')
(x : ๐)
:
theorem
logDeriv_eq_zero_of_not_differentiableAt
{๐ : Type u_1}
{๐' : Type u_2}
[NontriviallyNormedField ๐]
[NontriviallyNormedField ๐']
[NormedAlgebra ๐ ๐']
(f : ๐ โ ๐')
(x : ๐)
(h : ยฌDifferentiableAt ๐ f x)
:
@[simp]
@[simp]
@[simp]
theorem
logDeriv_const
{๐ : Type u_1}
{๐' : Type u_2}
[NontriviallyNormedField ๐]
[NontriviallyNormedField ๐']
[NormedAlgebra ๐ ๐']
(a : ๐')
:
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)
:
theorem
logDeriv_mul_const
{๐ : Type u_1}
{๐' : Type u_2}
[NontriviallyNormedField ๐]
[NontriviallyNormedField ๐']
[NormedAlgebra ๐ ๐']
{f : ๐ โ ๐'}
(x : ๐)
(a : ๐')
(ha : a โ 0)
:
theorem
logDeriv_const_mul
{๐ : Type u_1}
{๐' : Type u_2}
[NontriviallyNormedField ๐]
[NontriviallyNormedField ๐']
[NormedAlgebra ๐ ๐']
{f : ๐ โ ๐'}
(x : ๐)
(a : ๐')
(ha : a โ 0)
:
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)
:
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 : โค)
:
theorem
logDeriv_fun_pow
{๐ : Type u_1}
{๐' : Type u_2}
[NontriviallyNormedField ๐]
[NontriviallyNormedField ๐']
[NormedAlgebra ๐ ๐']
{f : ๐ โ ๐'}
{x : ๐}
(hdf : DifferentiableAt ๐ f x)
(n : โ)
:
@[simp]
@[simp]
@[simp]
theorem
logDeriv_comp
{๐ : Type u_1}
{๐' : Type u_2}
[NontriviallyNormedField ๐]
[NontriviallyNormedField ๐']
[NormedAlgebra ๐ ๐']
{f : ๐' โ ๐'}
{g : ๐ โ ๐'}
{x : ๐}
(hf : DifferentiableAt ๐' f (g x))
(hg : DifferentiableAt ๐ g x)
: