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.

def LineDeriv.iteratedLineDerivOp {V : Type u_11} {E : Type u_12} [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.

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

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

@[simp]

theorem LineDeriv.iteratedLineDerivOp_fin_zero {V : Type u_11} {E : Type u_12} [LineDeriv V E E] (m : Fin 0 → V) (f : E) : iteratedLineDerivOp m f = f

@[simp]

theorem LineDeriv.iteratedLineDerivOp_one {V : Type u_11} {E : Type u_12} [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_11} {E : Type u_12} [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_11} {E : Type u_12} [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_11} {E : Type u_12} [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_11) (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_11) (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)

@[simp]

theorem LineDeriv.lineDerivOp_zero {V : Type u_5} {E : Type u_6} {F : Type u_7} [AddCommGroup V] [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] [LineDerivAdd V E F] (v : V) : lineDerivOp v 0 = 0

@[simp]

theorem LineDeriv.lineDerivOp_neg {V : Type u_5} {E : Type u_6} {F : Type u_7} [AddCommGroup V] [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] [LineDerivAdd V E F] (v : V) (x : E) : lineDerivOp v (-x) = -lineDerivOp v x

@[simp]

theorem LineDeriv.lineDerivOp_sum {ι : Type u_1} {V : Type u_5} {E : Type u_6} {F : Type u_7} [AddCommGroup V] [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] [LineDerivAdd V E F] (v : V) (f : ι → E) (s : Finset ι) : lineDerivOp v (∑ i ∈ s, f i) = ∑ i ∈ s, lineDerivOp v (f i)

@[simp]

theorem LineDeriv.lineDerivOp_left_zero {V : Type u_5} {E : Type u_6} {F : Type u_7} [AddCommGroup V] [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] [LineDerivAdd V E F] (x : E) : lineDerivOp 0 x = 0

@[simp]

theorem LineDeriv.lineDerivOp_left_neg {V : Type u_5} {E : Type u_6} {F : Type u_7} [AddCommGroup V] [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] [LineDerivAdd V E F] (v : V) (x : E) : lineDerivOp (-v) x = -lineDerivOp v x

@[simp]

theorem LineDeriv.lineDerivOp_left_sum {ι : Type u_1} {V : Type u_5} {E : Type u_6} {F : Type u_7} [AddCommGroup V] [AddCommGroup E] [AddCommGroup F] [LineDeriv V E F] [LineDerivAdd V E F] (f : ι → V) (x : E) (s : Finset ι) : lineDerivOp (∑ i ∈ s, f i) x = ∑ i ∈ s, lineDerivOp (f i) x

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.

@[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

@[simp]

theorem LineDeriv.iteratedLineDerivOp_zero {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] : iteratedLineDerivOp m 0 = 0

@[simp]

theorem LineDeriv.iteratedLineDerivOp_neg {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 : E) : iteratedLineDerivOp m (-x) = -iteratedLineDerivOp m x

@[simp]

theorem LineDeriv.iteratedLineDerivOp_sum {ι : Type u_1} {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] (f : ι → E) (s : Finset ι) : iteratedLineDerivOp m (∑ i ∈ s, f i) = ∑ i ∈ s, iteratedLineDerivOp m (f i)

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.

@[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.

Laplacian of LineDeriv

def LineDeriv.bilinearLineDerivTwo (R : Type u_4) {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [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.

def LineDeriv.tensorLineDerivTwo (R : Type u_4) {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [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.

theorem LineDeriv.tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp {R : Type u_4} {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [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_8} {V₂ : Type u_9} {V₃ : Type u_10} [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_8) {V₂ : Type u_9} {V₃ : Type u_10} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CommRing R] [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.

theorem LineDeriv.laplacianCLM_eq_sum {ι : Type u_1} {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [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)