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
  • A.5. Constant of time deriative and space derivatives zero
  • A.6. Equal up to a constant of time and space derivatives equal
• B. Derivatives of distributions on Time × Space d
  • B.1. Time derivatives
    • B.1.1. Composition with a CLM
  • B.2. Space derivatives
    • B.2.1. Space derivatives commute
    • B.2.2. Composition with a CLM
  • 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.

A.5. Constant of time deriative and space derivatives zero

theorem Space.space_fun_of_time_deriv_eq_zero {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {f : Time → Space d → M} (hf : Differentiable ℝ ↿f) (h : ∀ (t : Time) (x : Space d), Time.deriv (fun (x_1 : Time) => f x_1 x) t = 0) : ∃ (g : Space d → M), ∀ (t : Time) (x : Space d), f t x = g x

theorem Space.time_fun_of_space_deriv_eq_zero {d : ℕ} {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {f : Time → Space d → M} (hf : Differentiable ℝ ↿f) (h : ∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0) : ∃ (g : Time → M), ∀ (t : Time) (x : Space d), f t x = g t

theorem Space.const_of_time_deriv_space_deriv_eq_zero {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {f : Time → Space d → M} (hf : Differentiable ℝ ↿f) (h₁ : ∀ (t : Time) (x : Space d), Time.deriv (fun (x_1 : Time) => f x_1 x) t = 0) (h₂ : ∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = 0) : ∃ (c : M), ∀ (t : Time) (x : Space d), f t x = c

A.6. Equal up to a constant of time and space derivatives equal

theorem Space.equal_up_to_const_of_deriv_eq {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {f g : Time → Space d → M} (hf : Differentiable ℝ ↿f) (hg : Differentiable ℝ ↿g) (h₁ : ∀ (t : Time) (x : Space d), Time.deriv (fun (x_1 : Time) => f x_1 x) t = Time.deriv (fun (x_1 : Time) => g x_1 x) t) (h₂ : ∀ (t : Time) (x : Space d) (i : Fin d), deriv i (f t) x = deriv i (g t) x) : ∃ (c : M), ∀ (t : Time) (x : Space d), f t x = g t x + c

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)

theorem Space.distTimeDeriv_apply' {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : (Time × Space d)→d[ℝ] M) (ε : SchwartzMap (Time × Space d) ℝ) : (distTimeDeriv f) ε = -f ((SchwartzMap.evalCLM (1, 0)) ((SchwartzMap.fderivCLM ℝ) ε))

theorem Space.apply_fderiv_eq_distTimeDeriv {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : (Time × Space d)→d[ℝ] M) (ε : SchwartzMap (Time × Space d) ℝ) : f ((SchwartzMap.evalCLM (1, 0)) ((SchwartzMap.fderivCLM ℝ) ε)) = -(distTimeDeriv f) ε

B.1.1. Composition with a CLM

theorem Space.distTimeDeriv_apply_CLM {M M2 : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] [NormedAddCommGroup M2] [NormedSpace ℝ M2] (f : (Time × Space d)→d[ℝ] M) (c : M →L[ℝ] M2) : distTimeDeriv (c.comp f) = c.comp (distTimeDeriv f)

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)

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) ε = -f ((SchwartzMap.evalCLM (0, basis i)) ((SchwartzMap.fderivCLM ℝ) ε))

theorem Space.apply_fderiv_eq_distSpaceDeriv {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) (f : (Time × Space d)→d[ℝ] M) (ε : SchwartzMap (Time × Space d) ℝ) : f ((SchwartzMap.evalCLM (0, basis i)) ((SchwartzMap.fderivCLM ℝ) ε)) = -((distSpaceDeriv i) f) ε

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.2.2. Composition with a CLM

theorem Space.distSpaceDeriv_apply_CLM {M M2 : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] [NormedAddCommGroup M2] [NormedSpace ℝ M2] (i : Fin d) (f : (Time × Space d)→d[ℝ] M) (c : M →L[ℝ] M2) : (distSpaceDeriv i) (c.comp f) = c.comp ((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) ε).ofLp = 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) η).ofLp 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.