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.

source

def Differential.logDeriv {R : Type u_1} [Field R] [Differential R] (a : R) :

The logarithmic derivative of a is a′ / a.

Equations

Differential.logDeriv a = a′ / a

source

@[simp]

theorem Differential.logDeriv_zero {R : Type u_1} [Field R] [Differential R] :

logDeriv 0 = 0

source

@[simp]

theorem Differential.logDeriv_one {R : Type u_1} [Field R] [Differential R] :

logDeriv 1 = 0

source

theorem Differential.logDeriv_mul {R : Type u_1} [Field R] [Differential R] (a b : R) (ha : a ≠ 0) (hb : b ≠ 0) :

logDeriv (a * b) = logDeriv a + logDeriv b

source

theorem Differential.logDeriv_div {R : Type u_1} [Field R] [Differential R] (a b : R) (ha : a ≠ 0) (hb : b ≠ 0) :

logDeriv (a / b) = logDeriv a - logDeriv b

source

@[simp]

theorem Differential.logDeriv_pow {R : Type u_1} [Field R] [Differential R] (n : ℕ) (a : R) :

logDeriv (a ^ n) = ↑n * logDeriv a

source

theorem Differential.logDeriv_eq_zero {R : Type u_1} [Field R] [Differential R] (a : R) :

logDeriv a = 0 ↔ a′ = 0

source

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) :

logDeriv (Multiset.map f s).prod = (Multiset.map (fun (x : ι) => logDeriv (f x)) s).sum

source

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) :

logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, logDeriv (f x)

source

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) :

logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, logDeriv (f x)

source

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) :

logDeriv ((algebraMap F K) a) = (algebraMap F K) (logDeriv a)

source

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) :

↑(Differential.logDeriv a) = Differential.logDeriv ↑a

source

noncomputable instance Differential.instAdjoinRootOfIrreduciblePolynomialOfFactMonic {F : Type u_2} [Field F] [Differential F] [CharZero F] (p : Polynomial F) [Fact (Irreducible p)] [Fact p.Monic] :

Differential (AdjoinRoot p)

Equations

Differential.instAdjoinRootOfIrreduciblePolynomialOfFactMonic p = { deriv := Derivation.liftOfSurjective ⋯ ⋯ }

source

instance Differential.instDifferentialAlgebraAdjoinRoot {F : Type u_2} [Field F] [Differential F] [CharZero F] (p : Polynomial F) [Fact (Irreducible p)] [Fact p.Monic] :

DifferentialAlgebra F (AdjoinRoot p)

source

@[reducible]

noncomputable def Differential.differentialFiniteDimensional (F : Type u_2) [Field F] [Differential F] [CharZero F] (K : Type u_3) [Field K] [Algebra F K] [FiniteDimensional F K] :

Differential K

If K is a finite field extension of F then we can define a differential algebra on K, by choosing a primitive element of K, k and then using the equivalence to AdjoinRoot (minpoly k).

Equations