Gradient of functions and distributions on Space d

i. Overview

This module defines and proves basic properties of the gradient operator on functions from Space d to ℝ and on distributions from Space d to ℝ.

The gradient operator returns a vector field whose components are the partial derivatives of the input function with respect to each spatial coordinate.

ii. Key results

• grad : The gradient operator on functions from Space d to ℝ.
• distGrad : The gradient operator on distributions from Space d to ℝ.

iii. Table of contents

• A. The gradient of functions on Space d
  • A.1. Gradient of the zero function
  • A.2. Gradient distributes over addition
  • A.3. Gradient of a constant function
  • A.4. Gradient distributes over scalar multiplication
  • A.5. Gradient distributes over negation
  • A.6. Expansion in terms of basis vectors
  • A.7. Components of the gradient
  • A.8. Inner product with a gradient
  • A.9. Gradient is equal to gradient from Mathlib
  • A.10. Value of gradient in the direction of the position vector
  • A.11. Gradient of the norm squared function
  • A.12. Gradient of the inner product function
  • A.13. Integrability with bounded functions
• B. Gradient of distributions
  • B.1. The definition
  • B.2. The gradient of inner products
  • B.3. The gradient as a sum over basis vectors
  • B.4. The underlying function of the gradient distribution
  • B.5. The gradient applied to a Schwartz function

iv. References

A. The gradient of functions on Space d

noncomputable def Space.grad {d : ℕ} (f : Space d → ℝ) : Space d → EuclideanSpace ℝ (Fin d)

The vector calculus operator grad.

Equations

• Space.grad f x i = Space.deriv i f x

def Space.«term∇» : Lean.ParserDescr

The vector calculus operator grad.

Equations

• Space.«term∇» = Lean.ParserDescr.node `Space.«term∇» 1024 (Lean.ParserDescr.symbol "∇")

A.1. Gradient of the zero function

@[simp]

theorem Space.grad_zero {d : ℕ} : grad 0 = 0

A.2. Gradient distributes over addition

theorem Space.grad_add {d : ℕ} (f1 f2 : Space d → ℝ) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : grad (f1 + f2) = grad f1 + grad f2

A.3. Gradient of a constant function

@[simp]

theorem Space.grad_const {d : ℕ} {c : ℝ} : (grad fun (x : Space d) => c) = 0

A.4. Gradient distributes over scalar multiplication

theorem Space.grad_smul {d : ℕ} (f : Space d → ℝ) (k : ℝ) (hf : Differentiable ℝ f) : grad (k • f) = k • grad f

A.5. Gradient distributes over negation

theorem Space.grad_neg {d : ℕ} (f : Space d → ℝ) : grad (-f) = -grad f

A.6. Expansion in terms of basis vectors

theorem Space.grad_eq_sum {d : ℕ} (f : Space d → ℝ) (x : Space d) : grad f x = ∑ i : Fin d, deriv i f x • basis i

A.7. Components of the gradient

theorem Space.grad_apply {d : ℕ} (f : Space d → ℝ) (x : Space d) (i : Fin d) : grad f x i = deriv i f x

A.8. Inner product with a gradient

theorem Space.grad_inner_eq {d : ℕ} (f : Space d → ℝ) (x y : Space d) : inner ℝ (grad f x) y = (fderiv ℝ f x) y

theorem Space.inner_grad_eq {d : ℕ} (f : Space d → ℝ) (x y : Space d) : inner ℝ x (grad f y) = (fderiv ℝ f y) x

A.9. Gradient is equal to gradient from Mathlib

theorem Space.grad_eq_gradiant {d : ℕ} (f : Space d → ℝ) : grad f = gradient f

A.10. Value of gradient in the direction of the position vector

theorem Space.grad_inner_space_unit_vector {d : ℕ} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) : inner ℝ (grad f x) (‖x‖⁻¹ • x) = _root_.deriv (fun (r : ℝ) => f (r • ‖x‖⁻¹ • x)) ‖x‖

The gradient in the direction of the space position.

theorem Space.grad_inner_space {d : ℕ} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) : inner ℝ (grad f x) x = ‖x‖ * _root_.deriv (fun (r : ℝ) => f (r • ‖x‖⁻¹ • x)) ‖x‖

A.11. Gradient of the norm squared function

theorem Space.grad_norm_sq {d : ℕ} (x : Space d) : grad (fun (x : Space d) => ‖x‖ ^ 2) x = 2 • x

A.12. Gradient of the inner product function

theorem Space.grad_inner {d : ℕ} : (grad fun (y : Space d) => inner ℝ y y) = fun (z : Space d) => 2 • z

The gradient of the inner product is given by 2 • x.

theorem Space.grad_inner_left {d : ℕ} (x : Space d) : (grad fun (y : Space d) => inner ℝ y x) = fun (x_1 : Space d) => x

theorem Space.grad_inner_right {d : ℕ} (x : Space d) : (grad fun (y : Space d) => inner ℝ x y) = fun (x_1 : Space d) => x

A.13. Integrability with bounded functions

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

B. Gradient of distributions

B.1. The definition

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

B.2. The gradient of inner products

theorem Space.distGrad_inner_eq {d : ℕ} (f : (Space d)→d[ℝ] ℝ) (η : SchwartzMap (Space d) ℝ) (y : EuclideanSpace ℝ (Fin d)) : inner ℝ ((distGrad f) η) y = (((Distribution.fderivD ℝ) f) η) y

theorem Space.distGrad_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) : distGrad f = g

B.3. The gradient as a sum over basis vectors

theorem Space.distGrad_eq_sum_basis {d : ℕ} (f : (Space d)→d[ℝ] ℝ) (η : SchwartzMap (Space d) ℝ) : (distGrad f) η = ∑ i : Fin d, -f ((SchwartzMap.evalCLM (basis i)) ((SchwartzMap.fderivCLM ℝ) η)) • basis i

B.4. The underlying function of the gradient distribution

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

B.5. The gradient applied to a Schwartz function

theorem Space.distGrad_apply {d : ℕ} (f : (Space d)→d[ℝ] ℝ) (ε : SchwartzMap (Space d) ℝ) : (distGrad f) ε = fun (i : Fin d) => ((distDeriv i) f) ε