The Laplacian operator on Space d

i. Overview

In this module we define the Laplacian operator on functions and vector-valued functions defined on Space d.

ii. Key results

• laplacian : The Laplacian operator on scalar functions on Space d.
• laplacianVec : The Laplacian operator on vector-valued functions on Space d.

iii. Table of contents

• A. Laplacian on functions to ℝ
  • A.1. Relation between laplacian and divergence of gradient
• B. Laplacian on vector valued functions

iv. References

A. Laplacian on functions to ℝ

noncomputable def Space.laplacian {d : ℕ} (f : Space d → ℝ) : Space d → ℝ

The scalar laplacian operator.

Equations

• Space.laplacian f x = ∑ i : Fin d, (fun (i : Fin d) (x : Space d) => Space.deriv i (Space.deriv i f) x) i x

def Space.termΔ : Lean.ParserDescr

The scalar laplacian operator.

Equations

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

A.1. Relation between laplacian and divergence of gradient

theorem Space.laplacian_eq_div_of_grad (f : Space → ℝ) : laplacian f = div (grad f)

B. Laplacian on vector valued functions

noncomputable def Space.laplacianVec {d : ℕ} (f : Space d → EuclideanSpace ℝ (Fin d)) : Space d → EuclideanSpace ℝ (Fin d)

The vector laplacianVec operator.

Equations

• Space.laplacianVec f x i = Space.laplacian ((fun (i : Fin d) (x : Space d) => Space.coord i (f x)) i) x

def Space.termΔ_1 : Lean.ParserDescr

The vector laplacianVec operator.

Equations

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