Distributions on space

In this module we define the derivatives, gradient, divergence and curl of distributions on Space.

Contrary to the usual definition of derivatives on functions, when working with distributions one does not need to check that the function is differentiable to perform basic operations. This has the consequence that in a lot of cases, distributions are in fact somewhat easier to work with than functions.

Examples of distributions

Distributions cover a wide range of objects that we use in physics.

• The dirac delta function.
• The potential 1/r (which is not defined at the origin).
• The Heaviside step function.
• Interfaces between materials, such as a charged sphere.

The constant distribution on space

noncomputable def Space.constD {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (d : ℕ) (m : M) : (Space d)→d[ℝ] M

The constant distribution from Space d to a module M associated with m : M.

Equations

• Space.constD d m = Distribution.const ℝ (Space d) m

Derivatives

noncomputable def Space.derivD {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin d) : ((Space d)→d[ℝ] M) →ₗ[ℝ] (Space d)→d[ℝ] M

Given a distribution (function) f : Space d →d[ℝ] M the derivative of f in direction μ.

Equations

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

theorem Space.schwartMap_fderiv_comm {d : ℕ} (μ ν : Fin d) (x : Space d) (η : SchwartzMap (Space d) ℝ) : ((SchwartzMap.evalCLM (basis μ)) ((SchwartzMap.fderivCLM ℝ) ((SchwartzMap.evalCLM (basis ν)) ((SchwartzMap.fderivCLM ℝ) η)))) x = ((SchwartzMap.evalCLM (basis ν)) ((SchwartzMap.fderivCLM ℝ) ((SchwartzMap.evalCLM (basis μ)) ((SchwartzMap.fderivCLM ℝ) η)))) x

theorem Space.derivD_comm {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ ν : Fin d) (f : (Space d)→d[ℝ] M) : (derivD ν) ((derivD μ) f) = (derivD μ) ((derivD ν) f)

@[simp]

theorem Space.derivD_constD {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin d) (m : M) : (derivD μ) (constD d m) = 0

The gradient

noncomputable def Space.gradD {d : ℕ} : ((Space d)→d[ℝ] ℝ) →ₗ[ℝ] (Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)

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

Equations

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

theorem Space.gradD_inner_eq {d : ℕ} (f : (Space d)→d[ℝ] ℝ) (η : SchwartzMap (Space d) ℝ) (y : EuclideanSpace ℝ (Fin d)) : inner ℝ ((gradD f) η) y = (((Distribution.fderivD ℝ) f) η) y

theorem Space.gradD_eq_sum_basis {d : ℕ} (f : (Space d)→d[ℝ] ℝ) (η : SchwartzMap (Space d) ℝ) : (gradD f) η = ∑ i : Fin d, -f ((SchwartzMap.evalCLM (basis i)) ((SchwartzMap.fderivCLM ℝ) η)) • basis i

@[simp]

theorem Space.gradD_constD {d : ℕ} (m : ℝ) : gradD (constD d m) = 0

The divergence

noncomputable def Space.divD {d : ℕ} : ((Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) →ₗ[ℝ] (Space d)→d[ℝ] ℝ

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

Equations

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

theorem Space.divD_apply_eq_sum_fderivD {d : ℕ} (f : (Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) (η : SchwartzMap (Space d) ℝ) : (divD f) η = ∑ i : Fin d, (((Distribution.fderivD ℝ) f) η) (basis i) i

@[simp]

theorem Space.divD_constD {d : ℕ} (m : EuclideanSpace ℝ (Fin d)) : divD (constD d m) = 0

The curl

noncomputable def Space.curlD : (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.

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

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

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

theorem Space.curlD_apply (f : Space→d[ℝ] EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap Space ℝ) : (curlD 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

@[simp]

theorem Space.curlD_constD (m : EuclideanSpace ℝ (Fin 3)) : curlD (constD 3 m) = 0

## Vector identities

@[simp]

theorem Space.curlD_gradD_eq_zero (f : Space→d[ℝ] ℝ) : curlD (gradD f) = 0

The curl of a grad is equal to zero.