Divergence on Space

i. Overview

In this module we define the divergence operator on functions and distributions from Space d to EuclideanSpace ℝ (Fin d), and prove various basic properties about it.

ii. Key results

• div : The divergence operator on functions from Space d to EuclideanSpace ℝ (Fin d).
• distDiv : The divergence operator on distributions from Space d to EuclideanSpace ℝ (Fin d).
• distDiv_ofFunction : The divergence of a distribution from a bounded function.

iii. Table of contents

• A. The divergence on functions
  • A.1. The divergence on the zero function
  • A.2. The divergence on a constant function
  • A.3. The divergence distributes over addition
  • A.4. The divergence distributes over scalar multiplication
  • A.5. The divergence of a linear map is a linear map
• B. Divergence of distributions
  • B.1. Basic equalities
  • B.2. Divergence on distributions from bounded functions

iv. References

A. The divergence on functions

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

The vector calculus operator div.

Equations

• Space.div f x = ∑ i : Fin d, (fun (i : Fin d) (x : Space d) => Space.deriv i ((fun (i : Fin d) (x : Space d) => Space.coord i (f x)) i) x) i x

def Space.divNotation : Lean.ParserDescr

The vector calculus operator div.

Equations

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

A.1. The divergence on the zero function

@[simp]

theorem Space.div_zero {d : ℕ} : div 0 = 0

A.2. The divergence on a constant function

@[simp]

theorem Space.div_const {d : ℕ} {v : EuclideanSpace ℝ (Fin d)} : (div fun (x : Space d) => v) = 0

A.3. The divergence distributes over addition

theorem Space.div_add {d : ℕ} (f1 f2 : Space d → EuclideanSpace ℝ (Fin d)) (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) : div (f1 + f2) = div f1 + div f2

A.4. The divergence distributes over scalar multiplication

theorem Space.div_smul {d : ℕ} (f : Space d → EuclideanSpace ℝ (Fin d)) (k : ℝ) (hf : Differentiable ℝ f) : div (k • f) = k • div f

A.5. The divergence of a linear map is a linear map

theorem Space.div_linear_map {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : W → Space → EuclideanSpace ℝ (Fin 3)) (hf : ∀ (w : W), Differentiable ℝ (f w)) (hf' : IsLinearMap ℝ f) : IsLinearMap ℝ fun (w : W) => div (f w)

B. Divergence of distributions

noncomputable def Space.distDiv {d : ℕ} : ((Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) →ₗ[ℝ] (Space d)→d[ℝ] ℝ

The divergence of a distribution (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)) as a distribution (Space d) →d[ℝ] ℝ.

Equations

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

B.1. Basic equalities

theorem Space.distDiv_apply_eq_sum_fderivD {d : ℕ} (f : (Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) (η : SchwartzMap (Space d) ℝ) : (distDiv f) η = ∑ i : Fin d, (((Distribution.fderivD ℝ) f) η) (basis i) i

theorem Space.distDiv_apply_eq_sum_distDeriv {d : ℕ} (f : (Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) (η : SchwartzMap (Space d) ℝ) : (distDiv f) η = ∑ i : Fin d, ((distDeriv i) f) η i

B.2. Divergence on distributions from bounded functions

theorem Space.distDiv_ofFunction {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)) ℝ) : (distDiv (Distribution.ofFunction f hf hae)) η = -∫ (x : Space dm1.succ), inner ℝ (f x) (grad (⇑η) x)

The divergence of a distribution from a bounded function.