Type classes for derivatives

In this file we define notation type classes for line derivatives, also known as partial derivatives.

Moreover, we provide type-classes that encode the linear structure.

Currently, this type class is only used by Schwartz functions. Future uses include derivatives on test functions, distributions, tempered distributions, and Sobolev spaces (and other generalized function spaces).

class LineDeriv (V : Type u) (E : Type v) (F : outParam (Type w)) : Type (max (max u v) w)

The notation typeclass for the line derivative.

• lineDerivOp : V → E → F

  ∂_{v} f is the line derivative of f in direction v. The meaning of this notation is type-dependent.

def LineDeriv.«term∂_{_}» : Lean.ParserDescr

∂_{v} f is the line derivative of f in direction v. The meaning of this notation is type-dependent.

Equations

• One or more equations did not get rendered due to their size.

def LineDeriv.iteratedLineDerivOp {V : Type u_5} {E : Type u_6} [LineDeriv V E E] {n : ℕ} : (Fin n → V) → E → E

∂^{m} f is the iterated line derivative of f, where m is a finite number of (different) directions.

Equations

• One or more equations did not get rendered due to their size.

def LineDeriv.«term∂^{_}» : Lean.ParserDescr

∂^{m} f is the iterated line derivative of f, where m is a finite number of (different) directions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LineDeriv.iteratedLineDerivOp_zero {V : Type u_5} {E : Type u_6} [LineDeriv V E E] (m : Fin 0 → V) (f : E) : iteratedLineDerivOp m f = f

@[simp]

theorem LineDeriv.iteratedLineDerivOp_one {V : Type u_5} {E : Type u_6} [LineDeriv V E E] (m : Fin 1 → V) (f : E) : iteratedLineDerivOp m f = lineDerivOp (m 0) f

theorem LineDeriv.iteratedLineDerivOp_succ_left {V : Type u_5} {E : Type u_6} [LineDeriv V E E] {n : ℕ} (m : Fin (n + 1) → V) (f : E) : iteratedLineDerivOp m f = lineDerivOp (m 0) (iteratedLineDerivOp (Fin.tail m) f)

theorem LineDeriv.iteratedLineDerivOp_succ_right {V : Type u_5} {E : Type u_6} [LineDeriv V E E] {n : ℕ} (m : Fin (n + 1) → V) (f : E) : iteratedLineDerivOp m f = iteratedLineDerivOp (Fin.init m) (lineDerivOp (m (Fin.last n)) f)

@[simp]

theorem LineDeriv.iteratedLineDerivOp_const_eq_iter_lineDerivOp {V : Type u_5} {E : Type u_6} [LineDeriv V E E] (n : ℕ) (y : V) (f : E) : iteratedLineDerivOp (fun (x : Fin n) => y) f = (lineDerivOp y)^[n] f

class LineDerivAdd (V : Type u) (E : Type v) (F : outParam (Type w)) [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] : Prop

The line derivative is additive, ∂_{v} (x + y) = ∂_{v} x + ∂_{v} y for all x y : E.

Note that lineDeriv on functions is not additive.

• lineDerivOp_add (v : V) (x y : E) : LineDeriv.lineDerivOp v (x + y) = LineDeriv.lineDerivOp v x + LineDeriv.lineDerivOp v y

class LineDerivSMul (R : Type u_5) (V : Type u) (E : Type v) (F : outParam (Type w)) [SMul R E] [SMul R F] [LineDeriv V E F] : Prop

The line derivative commutes with scalar multiplication, ∂_{v} (r • x) = r • ∂_{v} x for all r : R and x : E.

• lineDerivOp_smul (v : V) (r : R) (x : E) : LineDeriv.lineDerivOp v (r • x) = r • LineDeriv.lineDerivOp v x

class ContinuousLineDeriv (V : Type u) (E : Type v) (F : outParam (Type w)) [TopologicalSpace E] [TopologicalSpace F] [LineDeriv V E F] : Prop

The line derivative is continuous.

• continuous_lineDerivOp (v : V) : Continuous (LineDeriv.lineDerivOp v)

def LineDeriv.lineDerivOpCLM (R : Type u_1) {V : Type u_2} (E : Type u_3) {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [LineDeriv V E F] [LineDerivAdd V E F] [LineDerivSMul R V E F] [ContinuousLineDeriv V E F] (m : V) : E →L[R] F

The line derivative as a continuous linear map.

Equations

• LineDeriv.lineDerivOpCLM R E m = { toFun := LineDeriv.lineDerivOp m, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem LineDeriv.lineDerivOpCLM_apply {R : Type u_1} {V : Type u_2} {E : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [LineDeriv V E F] [LineDerivAdd V E F] [LineDerivSMul R V E F] [ContinuousLineDeriv V E F] (m : V) (x : E) : (lineDerivOpCLM R E m) x = lineDerivOp m x

theorem LineDeriv.iteratedLineDerivOp_add {V : Type u_2} {E : Type u_3} [LineDeriv V E E] {n : ℕ} (m : Fin n → V) [AddCommGroup E] [LineDerivAdd V E E] (x y : E) : iteratedLineDerivOp m (x + y) = iteratedLineDerivOp m x + iteratedLineDerivOp m y

theorem LineDeriv.iteratedLineDerivOp_smul {R : Type u_1} {V : Type u_2} {E : Type u_3} [LineDeriv V E E] {n : ℕ} (m : Fin n → V) [SMul R E] [LineDerivSMul R V E E] (r : R) (x : E) : iteratedLineDerivOp m (r • x) = r • iteratedLineDerivOp m x

theorem LineDeriv.continuous_iteratedLineDerivOp {V : Type u_2} {E : Type u_3} [LineDeriv V E E] [TopologicalSpace E] [ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) : Continuous (iteratedLineDerivOp m)

def LineDeriv.iteratedLineDerivOpCLM (R : Type u_1) {V : Type u_2} (E : Type u_3) [LineDeriv V E E] [TopologicalSpace E] [Ring R] [AddCommGroup E] [Module R E] [LineDerivAdd V E E] [LineDerivSMul R V E E] [ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) : E →L[R] E

The iterated line derivative as a continuous linear map.

Equations

• LineDeriv.iteratedLineDerivOpCLM R E m = { toFun := LineDeriv.iteratedLineDerivOp m, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem LineDeriv.iteratedLineDerivOpCLM_apply {R : Type u_1} {V : Type u_2} {E : Type u_3} [LineDeriv V E E] [TopologicalSpace E] [Ring R] [AddCommGroup E] [Module R E] [LineDerivAdd V E E] [LineDerivSMul R V E E] [ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) (x : E) : (iteratedLineDerivOpCLM R E m) x = iteratedLineDerivOp m x