Functions and distributions on Time and Space d

i. Overview

In this module we define and prove basic lemmas about derivatives of functions and distributions on both Time and Space d.

We put these results in the namespace Space by convention.

ii. Key results

• distTimeDeriv : The derivative of a distribution on Time × Space d along the temporal coordinate.
• distSpaceDeriv : The derivative of a distribution on Time × Space d along the spatial i coordinate.
• distSpaceGrad : The spatial gradient of a distribution on Time × Space d.
• distSpaceDiv : The spatial divergence of a distribution on Time × Space d.
• distSpaceCurl : The spatial curl of a distribution on Time × Space 3.

iii. Table of contents

• A. Derivatives involving time and space
  • A.1. Space and time derivatives in terms of curried functions
  • A.2. Commuting time and space derivatives
  • A.3. Differentiablity conditions
  • A.4. Time derivative commute with curl
• B. Derivatives of distributions on Time × Space d
  • B.1. Time derivatives
  • B.2. Space derivatives
    • B.2.1. Space derivatives commute
  • B.3. Time and space derivatives commute
  • B.4. The spatial gradient
  • B.5. The spatial divergence
  • B.6. The spatial curl

iv. References

A. Derivatives involving time and space

A.1. Space and time derivatives in terms of curried functions

theorem Space.fderiv_space_eq_fderiv_curry {d : ℕ} {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → Space d → M) (t : Time) (x dx : Space d) (hf : Differentiable ℝ ↿f) : (fderiv ℝ (fun (x' : Space d) => f t x') x) dx = (fderiv ℝ ↿f (t, x)) (0, dx)

theorem Space.fderiv_time_eq_fderiv_curry {d : ℕ} {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → Space d → M) (t dt : Time) (x : Space d) (hf : Differentiable ℝ ↿f) : (fderiv ℝ (fun (t' : Time) => f t' x) t) dt = (fderiv ℝ ↿f (t, x)) (dt, 0)

A.2. Commuting time and space derivatives

theorem Space.fderiv_time_commute_fderiv_space {d : ℕ} {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → Space d → M) (t dt : Time) (x dx : Space d) (hf : ContDiff ℝ 2 ↿f) : (fderiv ℝ (fun (t' : Time) => (fderiv ℝ (fun (x' : Space d) => f t' x') x) dx) t) dt = (fderiv ℝ (fun (x' : Space d) => (fderiv ℝ (fun (t' : Time) => f t' x') t) dt) x) dx

Derivatives along space coordinates and time commute.

theorem Space.time_deriv_comm_space_deriv {d : ℕ} {i : Fin d} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {f : Time → Space d → M} (hf : ContDiff ℝ 2 ↿f) (t : Time) (x : Space d) : Time.deriv (fun (t' : Time) => deriv i (f t') x) t = deriv i (fun (x' : Space d) => Time.deriv (fun (t' : Time) => f t' x') t) x

A.3. Differentiablity conditions

theorem Space.space_deriv_differentiable_time {d : ℕ} {i : Fin d} {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {f : Time → Space d → M} (hf : ContDiff ℝ 2 ↿f) (x : Space d) : Differentiable ℝ fun (t : Time) => deriv i (f t) x

theorem Space.time_deriv_differentiable_space {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {f : Time → Space d → M} (hf : ContDiff ℝ 2 ↿f) (t : Time) : Differentiable ℝ fun (x : Space d) => Time.deriv (fun (x_1 : Time) => f x_1 x) t

theorem Space.curl_differentiable_time (fₜ : Time → Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 ↿fₜ) (x : Space) : Differentiable ℝ fun (t : Time) => curl (fₜ t) x

A.4. Time derivative commute with curl

theorem Space.time_deriv_curl_commute (fₜ : Time → Space → EuclideanSpace ℝ (Fin 3)) (t : Time) (x : Space) (hf : ContDiff ℝ 2 ↿fₜ) : Time.deriv (fun (t : Time) => curl (fₜ t) x) t = curl (fun (x : Space) => Time.deriv (fun (t : Time) => fₜ t x) t) x

Curl and time derivative commute.

B. Derivatives of distributions on Time × Space d

B.1. Time derivatives

noncomputable def Space.distTimeDeriv {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.distTimeDeriv_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : (Time × Space d)→d[ℝ] M) (ε : SchwartzMap (Time × Space d) ℝ) : (distTimeDeriv f) ε = (((Distribution.fderivD ℝ) f) ε) (1, 0)

B.2. Space derivatives

noncomputable def Space.distSpaceDeriv {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.distSpaceDeriv_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) (f : (Time × Space d)→d[ℝ] M) (ε : SchwartzMap (Time × Space d) ℝ) : ((distSpaceDeriv i) f) ε = (((Distribution.fderivD ℝ) f) ε) (0, basis i)

B.2.1. Space derivatives commute

theorem Space.distSpaceDeriv_commute {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i j : Fin d) (f : (Time × Space d)→d[ℝ] M) : (distSpaceDeriv i) ((distSpaceDeriv j) f) = (distSpaceDeriv j) ((distSpaceDeriv i) f)

B.3. Time and space derivatives commute

theorem Space.distTimeDeriv_commute_distSpaceDeriv {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) (f : (Time × Space d)→d[ℝ] M) : distTimeDeriv ((distSpaceDeriv i) f) = (distSpaceDeriv i) (distTimeDeriv f)

B.4. The spatial gradient

noncomputable def Space.distSpaceGrad {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.distSpaceGrad_apply {d : ℕ} (f : (Time × Space d)→d[ℝ] ℝ) (ε : SchwartzMap (Time × Space d) ℝ) : (distSpaceGrad f) ε = fun (i : Fin d) => ((distSpaceDeriv i) f) ε

B.5. The spatial divergence

noncomputable def Space.distSpaceDiv {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.distSpaceDiv_apply_eq_sum_distSpaceDeriv {d : ℕ} (f : (Time × Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) (η : SchwartzMap (Time × Space d) ℝ) : (distSpaceDiv f) η = ∑ i : Fin d, ((distSpaceDeriv i) f) η i

B.6. The spatial curl

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