Type classes for derivatives and the Laplacian

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

Moreover, we provide type-classes that encode the linear structure. We also define the iterated line derivative and prove elementary properties. We define a Laplacian based on the sum of second derivatives formula and prove that the Laplacian thus defined is independent of the choice of basis.

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

Line derivative

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_14} {E : Type u_15} [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_14} {E : Type u_15} [LineDeriv V E E] (m : Fin 0 → V) (f : E) : iteratedLineDerivOp m f = f

@[simp]

theorem LineDeriv.iteratedLineDerivOp_one {V : Type u_14} {E : Type u_15} [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_14} {E : Type u_15} [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_14} {E : Type u_15} [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_14} {E : Type u_15} [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 V] [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 and ∂_{v + w} x = ∂_{v} x + ∂_{w} y for all v w : V.

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
• lineDerivOp_left_add (v w : V) (x : E) : LineDeriv.lineDerivOp (v + w) x = LineDeriv.lineDerivOp v x + LineDeriv.lineDerivOp w x

class LineDerivSMul (R : Type u_14) (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 LineDerivLeftSMul (R : Type u_14) (V : Type u) (E : Type v) (F : outParam (Type w)) [SMul R V] [SMul R F] [LineDeriv V E F] : Prop

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

• lineDerivOp_left_smul (r : R) (v : V) (x : E) : LineDeriv.lineDerivOp (r • v) 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_4) {V : Type u_5} (E : Type u_6) {F : Type u_7} [Ring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [AddCommGroup V] [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_4} {V : Type u_5} {E : Type u_6} {F : Type u_7} [Ring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] [AddCommGroup V] [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_5} {E : Type u_6} [LineDeriv V E E] {n : ℕ} (m : Fin n → V) [AddCommGroup 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_4} {V : Type u_5} {E : Type u_6} [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_5} {E : Type u_6} [LineDeriv V E E] [TopologicalSpace E] [ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) : Continuous (iteratedLineDerivOp m)

def LineDeriv.iteratedLineDerivOpCLM (R : Type u_4) {V : Type u_5} (E : Type u_6) [LineDeriv V E E] [TopologicalSpace E] [Ring R] [AddCommGroup V] [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_4} {V : Type u_5} {E : Type u_6} [LineDeriv V E E] [TopologicalSpace E] [Ring R] [AddCommGroup V] [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

Laplacian

class Laplacian (E : Type v) (F : outParam (Type w)) : Type (max v w)

The notation typeclass for the Laplace operator.

• laplacian : E → F

  Δ f is the Laplacian of f. The meaning of this notation is type-dependent.

def Laplacian.termΔ : Lean.ParserDescr

Δ f is the Laplacian of f. The meaning of this notation is type-dependent.

Equations

• Laplacian.termΔ = Lean.ParserDescr.node `Laplacian.termΔ 1024 (Lean.ParserDescr.symbol "Δ")

Laplacian of LineDeriv

def LineDeriv.bilinearLineDerivTwo (R : Type u_4) {E : Type u_6} {V₁ : Type u_11} {V₂ : Type u_12} {V₃ : Type u_13} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [CommRing R] [AddCommGroup E] [Module R E] [Module R V₂] [Module R V₃] [LineDerivAdd E V₂ V₃] [LineDerivAdd E V₁ V₂] [LineDerivSMul R E V₂ V₃] [LineDerivLeftSMul R E V₁ V₂] [LineDerivLeftSMul R E V₂ V₃] (f : V₁) : E →ₗ[R] E →ₗ[R] V₃

The second derivative in terms lineDerivOp as a bilinear map.

Mainly used to give an abstract definition of the Laplacian.

Equations

• LineDeriv.bilinearLineDerivTwo R f = LinearMap.mk₂ R (fun (x1 x2 : E) => LineDeriv.lineDerivOp x1 (LineDeriv.lineDerivOp x2 f)) ⋯ ⋯ ⋯ ⋯

def LineDeriv.tensorLineDerivTwo (R : Type u_4) {E : Type u_6} {V₁ : Type u_11} {V₂ : Type u_12} {V₃ : Type u_13} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [CommRing R] [AddCommGroup E] [Module R E] [Module R V₂] [Module R V₃] [LineDerivAdd E V₂ V₃] [LineDerivAdd E V₁ V₂] [LineDerivSMul R E V₂ V₃] [LineDerivLeftSMul R E V₁ V₂] [LineDerivLeftSMul R E V₂ V₃] (f : V₁) : TensorProduct R E E →ₗ[R] V₃

The second derivative in terms lineDerivOp as a linear map from the tensor product.

Mainly used to give an abstract definition of the Laplacian.

Equations

• LineDeriv.tensorLineDerivTwo R f = TensorProduct.lift (LineDeriv.bilinearLineDerivTwo R f)

theorem LineDeriv.tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp {R : Type u_4} {E : Type u_6} {V₁ : Type u_11} {V₂ : Type u_12} {V₃ : Type u_13} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [CommRing R] [AddCommGroup E] [Module R E] [Module R V₂] [Module R V₃] [LineDerivAdd E V₂ V₃] [LineDerivAdd E V₁ V₂] [LineDerivSMul R E V₂ V₃] [LineDerivLeftSMul R E V₁ V₂] [LineDerivLeftSMul R E V₂ V₃] (f : V₁) (v w : E) : (tensorLineDerivTwo R f) (v ⊗ₜ[R] w) = lineDerivOp v (lineDerivOp w f)

theorem LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum {ι : Type u_1} {E : Type u_6} {V₁ : Type u_11} {V₂ : Type u_12} {V₃ : Type u_13} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Module ℝ V₂] [Module ℝ V₃] [LineDerivAdd E V₁ V₂] [LineDerivAdd E V₂ V₃] [LineDerivSMul ℝ E V₂ V₃] [LineDerivLeftSMul ℝ E V₁ V₂] [LineDerivLeftSMul ℝ E V₂ V₃] [Fintype ι] (v : OrthonormalBasis ι ℝ E) (f : V₁) : (tensorLineDerivTwo ℝ f) (InnerProductSpace.canonicalCovariantTensor E) = ∑ i : ι, lineDerivOp (v i) (lineDerivOp (v i) f)

def LineDeriv.laplacianCLM (R : Type u_4) (E : Type u_6) (V₁ : Type u_11) {V₂ : Type u_12} {V₃ : Type u_13} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [CommRing R] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Module R V₁] [Module R V₂] [Module R V₃] [TopologicalSpace V₁] [TopologicalSpace V₂] [TopologicalSpace V₃] [IsTopologicalAddGroup V₃] [LineDerivAdd E V₁ V₂] [LineDerivSMul R E V₁ V₂] [ContinuousLineDeriv E V₁ V₂] [LineDerivAdd E V₂ V₃] [LineDerivSMul R E V₂ V₃] [ContinuousLineDeriv E V₂ V₃] : V₁ →L[R] V₃

The Laplacian defined by iterated lineDerivOp as a continuous linear map.

Equations

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

theorem LineDeriv.laplacianCLM_eq_sum {ι : Type u_1} {E : Type u_6} {V₁ : Type u_11} {V₂ : Type u_12} {V₃ : Type u_13} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Module ℝ V₁] [Module ℝ V₂] [Module ℝ V₃] [TopologicalSpace V₁] [TopologicalSpace V₂] [TopologicalSpace V₃] [IsTopologicalAddGroup V₃] [LineDerivAdd E V₁ V₂] [LineDerivSMul ℝ E V₁ V₂] [ContinuousLineDeriv E V₁ V₂] [LineDerivAdd E V₂ V₃] [LineDerivSMul ℝ E V₂ V₃] [ContinuousLineDeriv E V₂ V₃] [LineDerivLeftSMul ℝ E V₁ V₂] [LineDerivLeftSMul ℝ E V₂ V₃] [Fintype ι] (v : OrthonormalBasis ι ℝ E) (f : V₁) : (laplacianCLM ℝ E V₁) f = ∑ i : ι, lineDerivOp (v i) (lineDerivOp (v i) f)