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.

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

@[simp]

theorem LineDeriv.iteratedLineDerivOp_one {V : Type u_9} {E : Type u_10} [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_9} {E : Type u_10} [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_9} {E : Type u_10} [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_9} {E : Type u_10} [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_9) (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_9) (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_3} {E : Type u_4} {F : Type u_5} [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_3} {E : Type u_4} {F : Type u_5} [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_3} {E : Type u_4} {F : Type u_5} [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_3} {E : Type u_4} {F : Type u_5} [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_3} {E : Type u_4} {F : Type u_5} [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_3} {E : Type u_4} {F : Type u_5} [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_2) {V : Type u_3} (E : Type u_4) {F : Type u_5} [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_2} {V : Type u_3} {E : Type u_4} {F : Type u_5} [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_3} {E : Type u_4} [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_3} {E : Type u_4} [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_3} {E : Type u_4} [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_3} {E : Type u_4} [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_2} {V : Type u_3} {E : Type u_4} [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_3} {E : Type u_4} [LineDeriv V E E] [TopologicalSpace E] [ContinuousLineDeriv V E E] {n : ℕ} (m : Fin n → V) : Continuous (iteratedLineDerivOp m)

def LineDeriv.iteratedLineDerivOpCLM (R : Type u_2) {V : Type u_3} (E : Type u_4) [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_2} {V : Type u_3} {E : Type u_4} [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_2) {E : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [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_2) {E : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [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_2} {E : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [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_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [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)

noncomputable def LineDeriv.laplacianCLM (R : Type u_2) (E : Type u_4) (V₁ : Type u_6) {V₂ : Type u_7} {V₃ : Type u_8} [LineDeriv E V₁ V₂] [LineDeriv E V₂ V₃] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [CommRing R] [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

• LineDeriv.laplacianCLM R E V₁ = ∑ i : Fin (Module.finrank ℝ E), LineDeriv.lineDerivOpCLM R V₂ ((stdOrthonormalBasis ℝ E) i) ∘SL LineDeriv.lineDerivOpCLM R V₁ ((stdOrthonormalBasis ℝ E) i)

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