Differential Fields #
This file defines the logarithmic derivative Differential.logDeriv and proves properties of it.
This is defined algebraically, compared to logDeriv which is analytical.
@[simp]
@[simp]
theorem
Differential.logDeriv_mul
{R : Type u_1}
[Field R]
[Differential R]
(a : R)
(b : R)
(ha : a ≠ 0)
(hb : b ≠ 0)
:
theorem
Differential.logDeriv_div
{R : Type u_1}
[Field R]
[Differential R]
(a : R)
(b : R)
(ha : a ≠ 0)
(hb : b ≠ 0)
:
@[simp]
theorem
Differential.logDeriv_pow
{R : Type u_1}
[Field R]
[Differential R]
(n : ℕ)
(a : R)
:
Differential.logDeriv (a ^ n) = ↑n * Differential.logDeriv a
theorem
Differential.logDeriv_eq_zero
{R : Type u_1}
[Field R]
[Differential R]
(a : R)
:
Differential.logDeriv a = 0 ↔ a′ = 0
theorem
Differential.logDeriv_multisetProd
{R : Type u_1}
[Field R]
[Differential R]
{ι : Type u_2}
(s : Multiset ι)
{f : ι → R}
(h : ∀ x ∈ s, f x ≠ 0)
:
Differential.logDeriv (Multiset.map f s).prod = (Multiset.map (fun (x : ι) => Differential.logDeriv (f x)) s).sum
theorem
Differential.logDeriv_prod
{R : Type u_1}
[Field R]
[Differential R]
(ι : Type u_2)
(s : Finset ι)
(f : ι → R)
(h : ∀ x ∈ s, f x ≠ 0)
:
Differential.logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, Differential.logDeriv (f x)
theorem
Differential.logDeriv_prod_of_eq_zero
{R : Type u_1}
[Field R]
[Differential R]
(ι : Type u_2)
(s : Finset ι)
(f : ι → R)
(h : ∀ x ∈ s, f x = 0)
:
Differential.logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, Differential.logDeriv (f x)
theorem
Differential.logDeriv_algebraMap
{F : Type u_2}
{K : Type u_3}
[Field F]
[Field K]
[Differential F]
[Differential K]
[Algebra F K]
[DifferentialAlgebra F K]
(a : F)
:
Differential.logDeriv ((algebraMap F K) a) = (algebraMap F K) (Differential.logDeriv a)
theorem
algebraMap.coe_logDeriv
{F : Type u_2}
{K : Type u_3}
[Field F]
[Field K]
[Differential F]
[Differential K]
[Algebra F K]
[DifferentialAlgebra F K]
(a : F)
: