Curl on Space

i. Overview

In this module we define the curl of functions and distributions on 3-dimensional space Space 3.

We also prove some basic vector-identities involving of the curl operator.

ii. Key results

• curl : The curl operator on functions from Space 3 to EuclideanSpace ℝ (Fin 3).
• distCurl : The curl operator on distributions from Space 3 to EuclideanSpace ℝ (Fin 3).
• div_of_curl_eq_zero : The divergence of the curl of a function is zero.
• distCurl_distGrad_eq_zero : The curl of the gradient of a distribution is zero.

iii. Table of contents

• A. The curl on functions
  • A.1. The curl on the zero function
  • A.2. The curl on a constant function
  • A.3. The curl distributes over addition
  • A.4. The curl distributes over scalar multiplication
  • A.5. The curl of a linear map is a linear map
  • A.6. Preliminary lemmas about second derivatives
  • A.7. The div of a curl is zero
  • A.8. The curl of a curl
• B. The curl on distributions
  • B.1. The components of the curl
  • B.2. Basic equalities
  • B.3. The curl of a grad is zero

iv. References

A. The curl on functions

noncomputable def Space.curl (f : Space → EuclideanSpace ℝ (Fin 3)) : Space → EuclideanSpace ℝ (Fin 3)

The vector calculus operator curl.

Equations

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

def Space.curlNotation : Lean.ParserDescr

The vector calculus operator curl.

Equations

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

A.1. The curl on the zero function

@[simp]

theorem Space.curl_zero : curl 0 = 0

A.2. The curl on a constant function

@[simp]

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

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

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

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

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

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

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

B. The curl on distributions

noncomputable def Space.distCurl : (Space→d[ℝ] EuclideanSpace ℝ (Fin 3)) →ₗ[ℝ] Space→d[ℝ] EuclideanSpace ℝ (Fin 3)

The curl of a distribution Space →d[ℝ] (EuclideanSpace ℝ (Fin 3)) as a distribution Space →d[ℝ] (EuclideanSpace ℝ (Fin 3)).

Equations

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

B.1. The components of the curl

theorem Space.distCurl_apply_zero (f : Space→d[ℝ] EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap Space ℝ) : (distCurl f) η 0 = -f ((SchwartzMap.evalCLM (basis 2)) ((SchwartzMap.fderivCLM ℝ) η)) 1 + f ((SchwartzMap.evalCLM (basis 1)) ((SchwartzMap.fderivCLM ℝ) η)) 2

theorem Space.distCurl_apply_one (f : Space→d[ℝ] EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap Space ℝ) : (distCurl f) η 1 = -f ((SchwartzMap.evalCLM (basis 0)) ((SchwartzMap.fderivCLM ℝ) η)) 2 + f ((SchwartzMap.evalCLM (basis 2)) ((SchwartzMap.fderivCLM ℝ) η)) 0

theorem Space.distCurl_apply_two (f : Space→d[ℝ] EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap Space ℝ) : (distCurl f) η 2 = -f ((SchwartzMap.evalCLM (basis 1)) ((SchwartzMap.fderivCLM ℝ) η)) 0 + f ((SchwartzMap.evalCLM (basis 0)) ((SchwartzMap.fderivCLM ℝ) η)) 1

B.2. Basic equalities

theorem Space.distCurl_apply (f : Space→d[ℝ] EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap Space ℝ) : (distCurl f) η = fun (x : Fin 3) => match x with | 0 => -f ((SchwartzMap.evalCLM (basis 2)) ((SchwartzMap.fderivCLM ℝ) η)) 1 + f ((SchwartzMap.evalCLM (basis 1)) ((SchwartzMap.fderivCLM ℝ) η)) 2 | 1 => -f ((SchwartzMap.evalCLM (basis 0)) ((SchwartzMap.fderivCLM ℝ) η)) 2 + f ((SchwartzMap.evalCLM (basis 2)) ((SchwartzMap.fderivCLM ℝ) η)) 0 | 2 => -f ((SchwartzMap.evalCLM (basis 1)) ((SchwartzMap.fderivCLM ℝ) η)) 0 + f ((SchwartzMap.evalCLM (basis 0)) ((SchwartzMap.fderivCLM ℝ) η)) 1

B.3. The curl of a grad is zero

@[simp]

theorem Space.distCurl_distGrad_eq_zero (f : Space→d[ℝ] ℝ) : distCurl (distGrad f) = 0

The curl of a grad is equal to zero.