Derivatives on Space

i. Overview

In this module we define derivatives of functions and distributions on space Space d, in the standard directions.

ii. Key results

• deriv : The derivative of a function on space in a given direction.
• distDeriv : The derivative of a distribution on space in a given direction.

iii. Table of contents

• A. Derivatives of functions on Space d
  • A.1. Basic equalities
  • A.2. Derivative of the constant function
  • A.3. Derivative distributes over addition
  • A.4. Derivative distributes over scalar multiplication
  • A.5. Two spatial derivatives commute
  • A.6. Derivative of a component
  • A.7. Derivative of a component squared
  • A.8. Derivivatives of components
  • A.9. Derivative of a norm squared
    • A.9.1. Differentiability of the norm squared function
    • A.9.2. Derivative of the norm squared function
  • A.10. Derivative of the inner product
    • A.11.1. Differentiability of the inner product function
    • A.11.2. Derivative of the inner product function
  • A.12. Differentiability of derivatives
• B. Derivatives of distributions on Space d
  • B.1. The definition
  • B.2. Basic equality
  • B.3. Commutation of derivatives

iv. References

A. Derivatives of functions on Space d

noncomputable def Space.deriv {M : Type u_1} {d : ℕ} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (μ : Fin d) (f : Space d → M) : Space d → M

Given a function f : Space d → M the derivative of f in direction μ.

Equations

• Space.deriv μ f x = (fderiv ℝ f x) (EuclideanSpace.single μ 1)

def Space.«term∂[_]» : Lean.ParserDescr

Given a function f : Space d → M the derivative of f in direction μ.

Equations

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

A.1. Basic equalities

theorem Space.deriv_eq {M : Type u_1} {d : ℕ} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (μ : Fin d) (f : Space d → M) (x : Space d) : deriv μ f x = (fderiv ℝ f x) (EuclideanSpace.single μ 1)

theorem Space.deriv_eq_fderiv_basis {M : Type u_1} {d : ℕ} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (μ : Fin d) (f : Space d → M) (x : Space d) : deriv μ f x = (fderiv ℝ f x) (basis μ)

A.2. Derivative of the constant function

@[simp]

theorem Space.deriv_const {M : Type u_1} {d : ℕ} {t : Space d} [NormedAddCommGroup M] [NormedSpace ℝ M] (m : M) (μ : Fin d) : deriv μ (fun (x : Space d) => m) t = 0

A.3. Derivative distributes over addition

theorem Space.deriv_add {M : Type u_1} {d : ℕ} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f1 f2 : Space d → M) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : deriv u (f1 + f2) = deriv u f1 + deriv u f2

Derivatives on space distribute over addition.

theorem Space.deriv_coord_add {d : ℕ} {u i : Fin d} (f1 f2 : Space d → EuclideanSpace ℝ (Fin d)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : (deriv u fun (x : Space d) => f1 x i + f2 x i) = (deriv u fun (x : Space d) => f1 x i) + deriv u fun (x : Space d) => f2 x i

Derivatives on space distribute coordinate-wise over addition.

A.4. Derivative distributes over scalar multiplication

theorem Space.deriv_smul {M : Type u_1} {d : ℕ} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Space d → M) (k : ℝ) (hf : Differentiable ℝ f) : deriv u (k • f) = k • deriv u f

Scalar multiplication on space derivatives.

theorem Space.deriv_coord_smul {d : ℕ} {u i : Fin d} {x : Space d} (f : Space d → EuclideanSpace ℝ (Fin d)) (k : ℝ) (hf : Differentiable ℝ f) : deriv u (fun (x : Space d) => k * f x i) x = (k • deriv u fun (x : Space d) => f x i) x

Coordinate-wise scalar multiplication on space derivatives.

A.5. Two spatial derivatives commute

theorem Space.deriv_commute {M : Type u_1} {d : ℕ} {u v : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Space d → M) (hf : ContDiff ℝ 2 f) : deriv u (deriv v f) = deriv v (deriv u f)

Derivatives on space commute with one another.

A.6. Derivative of a component

@[simp]

theorem Space.deriv_component_same {d : ℕ} (μ : Fin d) (x : Space d) : deriv μ (fun (x : Space d) => x μ) x = 1

theorem Space.deriv_component_diff {d : ℕ} (μ ν : Fin d) (x : Space d) (h : μ ≠ ν) : deriv μ (fun (x : Space d) => x ν) x = 0

theorem Space.deriv_component {d : ℕ} (μ ν : Fin d) (x : Space d) : deriv ν (fun (x : Space d) => x μ) x = if ν = μ then 1 else 0

A.7. Derivative of a component squared

theorem Space.deriv_component_sq {d : ℕ} {ν μ : Fin d} (x : Space d) : deriv ν (fun (x : Space d) => x μ ^ 2) x = if ν = μ then 2 * x μ else 0

A.8. Derivivatives of components

theorem Space.deriv_euclid {n d : ℕ} {ν : Fin d} {μ : Fin n} {f : Space d → EuclideanSpace ℝ (Fin n)} (hf : Differentiable ℝ f) (x : Space d) : deriv ν (fun (x : Space d) => f x μ) x = deriv ν (fun (x : Space d) => f x) x μ

theorem Space.deriv_lorentz_vector {d : ℕ} {ν : Fin d} {μ : Fin 1 ⊕ Fin d} {f : Space d → Lorentz.Vector d} (hf : Differentiable ℝ f) (x : Space d) : deriv ν (fun (x : Space d) => f x μ) x = deriv ν (fun (x : Space d) => f x) x μ

A.9. Derivative of a norm squared

A.9.1. Differentiability of the norm squared function

theorem Space.norm_sq_differentiable {d : ℕ} : Differentiable ℝ fun (x : Space d) => ‖x‖ ^ 2

A.9.2. Derivative of the norm squared function

theorem Space.deriv_norm_sq {d : ℕ} (x : Space d) (i : Fin d) : deriv i (fun (x : Space d) => ‖x‖ ^ 2) x = 2 * x i

A.10. Derivative of the inner product

A.11.1. Differentiability of the inner product function

theorem Space.inner_differentiable {d : ℕ} : Differentiable ℝ fun (y : Space d) => inner ℝ y y

The inner product is differentiable.

A.11.2. Derivative of the inner product function

theorem Space.deriv_eq_inner_self {d : ℕ} (x : Space d) (i : Fin d) : deriv i (fun (x : Space d) => inner ℝ x x) x = 2 * x i

A.12. Differentiability of derivatives

theorem Space.deriv_differentiable {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} {f : Space d → M} (hf : ContDiff ℝ 2 f) (i : Fin d) : Differentiable ℝ (deriv i f)

B. Derivatives of distributions on Space d

B.1. The definition

noncomputable def Space.distDeriv {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.

B.2. Basic equality

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

B.3. Commutation of derivatives

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.distDeriv_commute {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ ν : Fin d) (f : (Space d)→d[ℝ] M) : (distDeriv ν) ((distDeriv μ) f) = (distDeriv μ) ((distDeriv ν) f)