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

theorem Space.derivD_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin d) (f : (Space d)→d[ℝ] M) (ε : SchwartzMap (Space d) ℝ) : ((derivD μ) f) ε = (((Distribution.fderivD ℝ) f) ε) (basis μ)

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_of_inner {d : ℕ} (f : (Space d)→d[ℝ] ℝ) (g : (Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) (h : ∀ (η : SchwartzMap (Space d) ℝ) (y : Space d), (((Distribution.fderivD ℝ) f) η) y = inner ℝ (g η) y) : gradD f = g

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

theorem Space.gradD_toFun_eq_derivD {d : ℕ} (f : (Space d)→d[ℝ] ℝ) : (↑(gradD f)).toFun = fun (ε : SchwartzMap (Space d) ℝ) (i : Fin d) => ((derivD i) f) ε

theorem Space.gradD_apply {d : ℕ} (f : (Space d)→d[ℝ] ℝ) (ε : SchwartzMap (Space d) ℝ) : (gradD f) ε = fun (i : Fin d) => ((derivD i) f) ε

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

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

@[simp]

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

theorem Space.divD_ofFunction {dm1 : ℕ} {f : Space dm1.succ → EuclideanSpace ℝ (Fin dm1.succ)} {hf : Distribution.IsDistBounded f} {hae : MeasureTheory.AEStronglyMeasurable (fun (x : Space dm1.succ) => f x) MeasureTheory.volume} (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) : (divD (Distribution.ofFunction f hf hae)) η = -∫ (x : Space dm1.succ), inner ℝ (f x) (grad (⇑η) x)

The divergence of a distribution from a bounded function.

theorem Space.integrable_isDistBounded_inner_grad_schwartzMap {dm1 : ℕ} {f : Space dm1.succ → EuclideanSpace ℝ (Fin dm1.succ)} (hf : Distribution.IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : Space dm1.succ) => f x) MeasureTheory.volume) (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) : MeasureTheory.Integrable (fun (x : Space dm1.succ) => inner ℝ (f x) (grad (⇑η) x)) MeasureTheory.volume

theorem Space.integrable_isDistBounded_inner_grad_schwartzMap_spherical {dm1 : ℕ} {f : Space dm1.succ → EuclideanSpace ℝ (Fin dm1.succ)} (hf : Distribution.IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : Space dm1.succ) => f x) MeasureTheory.volume) (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) : MeasureTheory.Integrable ((fun (x : ↑{0}ᶜ) => inner ℝ (f ↑x) (grad ⇑η ↑x)) ∘ ⇑(homeomorphUnitSphereProd (Space dm1.succ)).symm) (MeasureTheory.volume.toSphere.prod (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ (EuclideanSpace ℝ (Fin dm1.succ)) - 1)))

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.

For time-dependent distributions

noncomputable def Space.timeDerivD {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] : ((Time × Space d)→d[ℝ] M) →ₗ[ℝ] (Time × Space d)→d[ℝ] M

The time derivative of a distribution dependent on time and space.

Equations

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

theorem Space.timeDerivD_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : (Time × Space d)→d[ℝ] M) (ε : SchwartzMap (Time × Space d) ℝ) : (timeDerivD f) ε = (((Distribution.fderivD ℝ) f) ε) (1, 0)

noncomputable def Space.spaceDerivD {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) : ((Time × Space d)→d[ℝ] M) →ₗ[ℝ] (Time × Space d)→d[ℝ] M

The space derivative of a distribution dependent on time and space.

Equations

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

theorem Space.spaceDerivD_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) (f : (Time × Space d)→d[ℝ] M) (ε : SchwartzMap (Time × Space d) ℝ) : ((spaceDerivD i) f) ε = (((Distribution.fderivD ℝ) f) ε) (0, basis i)

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

The spatial gradient of a distribution dependent on time and space.

Equations

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

theorem Space.spaceGradD_apply {d : ℕ} (f : (Time × Space d)→d[ℝ] ℝ) (ε : SchwartzMap (Time × Space d) ℝ) : (spaceGradD f) ε = fun (i : Fin d) => ((spaceDerivD i) f) ε

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

The spatial divergence of a distribution dependent on time and space.

Equations

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

theorem Space.spaceDivD_apply_eq_sum_spaceDerivD {d : ℕ} (f : (Time × Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) (η : SchwartzMap (Time × Space d) ℝ) : (spaceDivD f) η = ∑ i : Fin d, ((spaceDerivD i) f) η i

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

The curl of a distribution dependent on time and space.

Equations

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