Vector identities

i. Overview

In this module we prove properties of the gradient, divergence, and curl operators. We show that on differentiable functions they are linear, show their action on basic functions, and prove vector calculus identities

ii. Key results

• grad_inner_space_unit_vector : The gradient in the direction of the space position.
• curl_of_curl : ∇ × (∇ × f) = ∇ (∇ ⬝ f) - Δ f
• div_of_curl_eq_zero : ∇ ⬝ (∇ × f) = 0

iii. Table of contents

• A. Basic lemmas about derivatives of space
  • A.1. Derivative distributes over addition
  • A.2. Derivative distributes over scalar multiplication
  • A.3. Two spatial derivatives commute
  • A.4. Derivative of a component
  • A.5. Derivative of a component squared
  • A.6. Derivative of a norm squared
    • A.6.1. Differentiability of the norm squared function
    • A.6.2. Derivative of the norm squared function
  • A.7. Derivative of the inner product
    • A.7.1. Differentiability of the inner product function
    • A.7.2. Derivative of the inner product function
• B. Properties of the gradient operator
  • B.1. Gradient of the zero function
  • B.2. Gradient distributes over addition
  • B.3. Gradient of a constant function
  • B.4. Gradient distributes over scalar multiplication
  • B.5. Gradient distributes over negation
  • B.6. Expansion in terms of basis vectors
  • B.7. Components of the gradient
  • B.8. Inner product with a gradient
  • B.9. Gradient is equal to gradient from Mathlib
  • B.10. Value of gradient in the direction of the position vector
  • B.11. Gradient of the norm squared function
  • B.12. Gradient of the inner product function
• C. Properties of the curl operator
  • C.1. The curl on the zero function
  • C.2. The curl on a constant function
  • C.3. The curl distributes over addition
  • C.4. The curl distributes over scalar multiplication
  • C.5. The curl of a linear map is a linear map
  • C.6. Preliminary lemmas about second derivatives
  • C.7. The div of a curl is zero
  • C.8. The curl of a curl
• D. Properties of the divergence operator
  • D.1. The divergence on the zero function
  • D.2. The divergence on a constant function
  • D.3. The divergence distributes over addition
  • D.4. The divergence distributes over scalar multiplication
  • D.5. The divergence of a linear map is a linear map
• E. Properties of the Laplacian operator

iv. References

A. Basic lemmas about derivatives of space

A.1. Derivative distributes over addition

theorem Space.deriv_add {M : Type u_1} {d : ℕ} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f1 f2 : Space d → M) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : deriv u (f1 + f2) = deriv u f1 + deriv u f2

Derivatives on space distribute over addition.

theorem Space.deriv_coord_add {d : ℕ} {u i : Fin d} (f1 f2 : Space d → EuclideanSpace ℝ (Fin d)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : (deriv u fun (x : Space d) => f1 x i + f2 x i) = (deriv u fun (x : Space d) => f1 x i) + deriv u fun (x : Space d) => f2 x i

Derivatives on space distribute coordinate-wise over addition.

A.2. Derivative distributes over scalar multiplication

theorem Space.deriv_smul {M : Type u_1} {d : ℕ} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Space d → M) (k : ℝ) (hf : Differentiable ℝ f) : deriv u (k • f) = k • deriv u f

Scalar multiplication on space derivatives.

theorem Space.deriv_coord_smul {d : ℕ} {u i : Fin d} {x : Space d} (f : Space d → EuclideanSpace ℝ (Fin d)) (k : ℝ) (hf : Differentiable ℝ f) : deriv u (fun (x : Space d) => k * f x i) x = (k • deriv u fun (x : Space d) => f x i) x

Coordinate-wise scalar multiplication on space derivatives.

A.3. Two spatial derivatives commute

theorem Space.deriv_commute {M : Type u_1} {d : ℕ} {u v : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Space d → M) (hf : ContDiff ℝ 2 f) : deriv u (deriv v f) = deriv v (deriv u f)

Derivatives on space commute with one another.

A.4. Derivative of a component

@[simp]

theorem Space.deriv_component_same {d : ℕ} (μ : Fin d) (x : Space d) : deriv μ (fun (x : Space d) => x μ) x = 1

theorem Space.deriv_component_diff {d : ℕ} (μ ν : Fin d) (x : Space d) (h : μ ≠ ν) : deriv μ (fun (x : Space d) => x ν) x = 0

theorem Space.deriv_component {d : ℕ} (μ ν : Fin d) (x : Space d) : deriv ν (fun (x : Space d) => x μ) x = if ν = μ then 1 else 0

A.5. Derivative of a component squared

theorem Space.deriv_component_sq {d : ℕ} {ν μ : Fin d} (x : Space d) : deriv ν (fun (x : Space d) => x μ ^ 2) x = if ν = μ then 2 * x μ else 0

A.6. Derivative of a norm squared

A.6.1. Differentiability of the norm squared function

theorem Space.norm_sq_differentiable {d : ℕ} : Differentiable ℝ fun (x : Space d) => ‖x‖ ^ 2

A.6.2. Derivative of the norm squared function

theorem Space.deriv_norm_sq {d : ℕ} (x : Space d) (i : Fin d) : deriv i (fun (x : Space d) => ‖x‖ ^ 2) x = 2 * x i

A.7. Derivative of the inner product

A.7.1. Differentiability of the inner product function

theorem Space.inner_differentiable {d : ℕ} : Differentiable ℝ fun (y : Space d) => inner ℝ y y

The inner product is differentiable.

A.7.2. Derivative of the inner product function

theorem Space.deriv_eq_inner_self {d : ℕ} (x : Space d) (i : Fin d) : deriv i (fun (x : Space d) => inner ℝ x x) x = 2 * x i

B. Properties of the gradient operator

B.1. Gradient of the zero function

@[simp]

theorem Space.grad_zero {d : ℕ} : grad 0 = 0

B.2. Gradient distributes over addition

theorem Space.grad_add {d : ℕ} (f1 f2 : Space d → ℝ) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : grad (f1 + f2) = grad f1 + grad f2

B.3. Gradient of a constant function

@[simp]

theorem Space.grad_const {d : ℕ} {c : ℝ} : (grad fun (x : Space d) => c) = 0

B.4. Gradient distributes over scalar multiplication

theorem Space.grad_smul {d : ℕ} (f : Space d → ℝ) (k : ℝ) (hf : Differentiable ℝ f) : grad (k • f) = k • grad f

B.5. Gradient distributes over negation

theorem Space.grad_neg {d : ℕ} (f : Space d → ℝ) : grad (-f) = -grad f

B.6. Expansion in terms of basis vectors

theorem Space.grad_eq_sum {d : ℕ} (f : Space d → ℝ) (x : Space d) : grad f x = ∑ i : Fin d, deriv i f x • basis i

B.7. Components of the gradient

theorem Space.grad_apply {d : ℕ} (f : Space d → ℝ) (x : Space d) (i : Fin d) : grad f x i = deriv i f x

B.8. Inner product with a gradient

theorem Space.grad_inner_eq {d : ℕ} (f : Space d → ℝ) (x y : Space d) : inner ℝ (grad f x) y = (fderiv ℝ f x) y

theorem Space.inner_grad_eq {d : ℕ} (f : Space d → ℝ) (x y : Space d) : inner ℝ x (grad f y) = (fderiv ℝ f y) x

B.9. Gradient is equal to gradient from Mathlib

theorem Space.grad_eq_gradiant {d : ℕ} (f : Space d → ℝ) : grad f = gradient f

B.10. Value of gradient in the direction of the position vector

theorem Space.grad_inner_space_unit_vector {d : ℕ} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) : inner ℝ (grad f x) (‖x‖⁻¹ • x) = _root_.deriv (fun (r : ℝ) => f (r • ‖x‖⁻¹ • x)) ‖x‖

The gradient in the direction of the space position.

theorem Space.grad_inner_space {d : ℕ} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) : inner ℝ (grad f x) x = ‖x‖ * _root_.deriv (fun (r : ℝ) => f (r • ‖x‖⁻¹ • x)) ‖x‖

B.11. Gradient of the norm squared function

theorem Space.grad_norm_sq {d : ℕ} (x : Space d) : grad (fun (x : Space d) => ‖x‖ ^ 2) x = 2 • x

B.12. Gradient of the inner product function

theorem Space.grad_inner {d : ℕ} : (grad fun (y : Space d) => inner ℝ y y) = fun (z : Space d) => 2 • z

The gradient of the inner product is given by 2 • x.

theorem Space.grad_inner_left {d : ℕ} (x : Space d) : (grad fun (y : Space d) => inner ℝ y x) = fun (x_1 : Space d) => x

theorem Space.grad_inner_right {d : ℕ} (x : Space d) : (grad fun (y : Space d) => inner ℝ x y) = fun (x_1 : Space d) => x

C. Properties of the curl operator

C.1. The curl on the zero function

@[simp]

theorem Space.curl_zero : curl 0 = 0

C.2. The curl on a constant function

@[simp]

theorem Space.curl_const {v₃ : EuclideanSpace ℝ (Fin 3)} : (curl fun (x : Space) => v₃) = 0

C.3. The curl distributes over addition

theorem Space.curl_add (f1 f2 : Space → EuclideanSpace ℝ (Fin 3)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : curl (f1 + f2) = curl f1 + curl f2

C.4. The curl distributes over scalar multiplication

theorem Space.curl_smul (f : Space → EuclideanSpace ℝ (Fin 3)) (k : ℝ) (hf : Differentiable ℝ f) : curl (k • f) = k • curl f

C.5. The curl of a linear map is a linear map

theorem Space.curl_linear_map {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : W → Space → EuclideanSpace ℝ (Fin 3)) (hf : ∀ (w : W), Differentiable ℝ (f w)) (hf' : IsLinearMap ℝ f) : IsLinearMap ℝ fun (w : W) => curl (f w)

C.6. Preliminary lemmas about second derivatives

theorem Space.deriv_coord_2nd_add {i u v w : Fin 3} (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : (deriv i fun (x : Space) => deriv u (fun (x : Space) => f x u) x + (deriv v (fun (x : Space) => f x v) x + deriv w (fun (x : Space) => f x w) x)) = deriv i (deriv u fun (x : Space) => f x u) + deriv i (deriv v fun (x : Space) => f x v) + deriv i (deriv w fun (x : Space) => f x w)

Second derivatives distribute coordinate-wise over addition (all three components for div).

theorem Space.deriv_coord_2nd_sub {u v w : Fin 3} (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : (deriv u fun (x : Space) => deriv v (fun (x : Space) => f x w) x - deriv w (fun (x : Space) => f x v) x) = deriv u (deriv v fun (x : Space) => f x w) - deriv u (deriv w fun (x : Space) => f x v)

Second derivatives distribute coordinate-wise over subtraction (two components for curl).

C.7. The div of a curl is zero

theorem Space.div_of_curl_eq_zero (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : div (curl f) = 0

C.8. The curl of a curl

theorem Space.curl_of_curl (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : curl (curl f) = grad (div f) - laplacianVec f

D. Properties of the divergence operator

D.1. The divergence on the zero function

@[simp]

theorem Space.div_zero {d : ℕ} : div 0 = 0

D.2. The divergence on a constant function

@[simp]

theorem Space.div_const {d : ℕ} {v : EuclideanSpace ℝ (Fin d)} : (div fun (x : Space d) => v) = 0

D.3. The divergence distributes over addition

theorem Space.div_add {d : ℕ} (f1 f2 : Space d → EuclideanSpace ℝ (Fin d)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : div (f1 + f2) = div f1 + div f2

D.4. The divergence distributes over scalar multiplication

theorem Space.div_smul {d : ℕ} (f : Space d → EuclideanSpace ℝ (Fin d)) (k : ℝ) (hf : Differentiable ℝ f) : div (k • f) = k • div f

D.5. The divergence of a linear map is a linear map

theorem Space.div_linear_map {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : W → Space → EuclideanSpace ℝ (Fin 3)) (hf : ∀ (w : W), Differentiable ℝ (f w)) (hf' : IsLinearMap ℝ f) : IsLinearMap ℝ fun (w : W) => div (f w)

E. Properties of the Laplacian operator

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