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.10.1. Differentiability of the inner product function
    • A.10.2. Derivative of the inner product function
    • A.10.3. Derivative of the inner product on one side
  • A.11. 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) (Space.basis μ)

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) (basis μ)

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

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 μ)

theorem Space.fderiv_eq_sum_deriv {M : Type u_1} {d : ℕ} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (f : Space d → M) (x y : Space d) : (fderiv ℝ f x) y = ∑ i : Fin d, y.val i • deriv i f x

theorem Space.deriv_eq_mfderiv {M : Type u_1} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin d) (f : Space d → M) (x : Space d) : deriv μ f x = (mfderiv (modelWithCornersSelf ℝ (Space d)) (modelWithCornersSelf ℝ M) f x) (basis μ)

The spatial-derivative in terms of the derivative of functions between manifolds.

theorem Space.mdifferentiable_manifoldStructure_iff_differentiable {M : Type u_1} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {f : Space d → M} {x : Space d} : MDifferentiableAt (manifoldStructure d) (modelWithCornersSelf ℝ M) f x ↔ DifferentiableAt ℝ f x

theorem Space.deriv_eq_mfderiv_manifoldStructure {M : Type u_1} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin d) (f : Space d → M) (x : Space d) : deriv μ f x = (mfderiv (manifoldStructure d) (modelWithCornersSelf ℝ M) f x) (EuclideanSpace.single μ 1)

The spatial-derivative in terms of the derivative of functions between manifolds with the manifold structure Space.manifoldStructure d.

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).ofLp i + (f2 x).ofLp i) = (deriv u fun (x : Space d) => (f1 x).ofLp i) + deriv u fun (x : Space d) => (f2 x).ofLp i

Derivatives on space distribute coordinate-wise over addition.

A.4. Derivative distributes over scalar multiplication

theorem Space.deriv_smul {M : Type u_1} {𝕜 : Type u_2} {d : ℕ} {x : Space d} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 M] {c : Space d → 𝕜} {f : Space d → M} (hc : DifferentiableAt ℝ c x) (hf : DifferentiableAt ℝ f x) : deriv u (c • f) x = c x • deriv u f x + deriv u c x • f x

Space derivatives on scalar product of functions.

theorem Space.deriv_const_smul {M : Type u_1} {R : Type u_2} {d : ℕ} {u : Fin d} [NormedAddCommGroup M] [NormedSpace ℝ M] [Semiring R] [Module R M] [SMulCommClass ℝ R M] [ContinuousConstSMul R M] {f : Space d → M} (c : R) (h : Differentiable ℝ f) : deriv u (c • f) = c • deriv u f

Space derivatives on scalar times function.

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).ofLp i) x = k * deriv u (fun (x : Space d) => (f x).ofLp 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.val μ) x = 1

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

theorem Space.deriv_component {d : ℕ} (μ ν : Fin d) (x : Space d) : deriv ν (fun (x : Space d) => x.val μ) 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.val μ ^ 2) x = if ν = μ then 2 * x.val μ 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).ofLp μ) x = (deriv ν (fun (x : Space d) => f x) x).ofLp μ

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.val i

A.10. Derivative of the inner product

A.10.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.

theorem Space.inner_differentiableAt {d : ℕ} (x : Space d) : DifferentiableAt ℝ (fun (y : Space d) => inner ℝ y y) x

theorem Space.inner_apply_differentiableAt {M : Type u_1} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {f g : M → Space d} (x : M) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : DifferentiableAt ℝ (fun (y : M) => inner ℝ (f y) (g y)) x

theorem Space.inner_apply_differentiable {M : Type u_1} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {f g : M → Space d} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) : Differentiable ℝ fun (y : M) => inner ℝ (f y) (g y)

theorem Space.inner_contDiff {n : WithTop ℕ∞} {d : ℕ} : ContDiff ℝ n fun (y : Space d) => inner ℝ y y

theorem Space.inner_apply_contDiff {M : Type u_1} {n : WithTop ℕ∞} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {f g : M → Space d} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) : ContDiff ℝ n fun (y : M) => inner ℝ (f y) (g y)

A.10.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.val i

A.10.3. Derivative of the inner product on one side

@[simp]

theorem Space.deriv_inner_left {d : ℕ} (x1 x2 : Space d) (i : Fin d) : deriv i (fun (x : Space d) => inner ℝ x x2) x1 = x2.val i

@[simp]

theorem Space.deriv_inner_right {d : ℕ} (x1 x2 : Space d) (i : Fin d) : deriv i (fun (x : Space d) => inner ℝ x1 x) x2 = x1.val i

A.11. 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 ℝ (Space d) ℝ (basis μ)) ((SchwartzMap.fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν)) ((SchwartzMap.fderivCLM ℝ (Space d) ℝ) η)))) x = ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis ν)) ((SchwartzMap.fderivCLM ℝ (Space d) ℝ) ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis μ)) ((SchwartzMap.fderivCLM ℝ (Space d) ℝ) η)))) 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)