The constant distribution on space

i. Overview

In this module we define the constant distribution from Space d to a module M. That is the distribution which sends every Schwartz function to its integral multiplied by a fixed element m : M.

We show that the derivatives of this constant distribution are zero.

ii. Key results

• distConst : The constant distribution from Space d to a module M.

iii. Table of contents

• A. The definition of the constant distribution
• B. Derivatives of the constant distribution

iv. References

A. The definition of the constant distribution

noncomputable def Space.distConst {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (d : ℕ) (m : M) : (Space d)→d[ℝ] M

The constant distribution from Space d to a module M associated with m : M.

Equations

• Space.distConst d m = Distribution.const ℝ (Space d) m

B. Derivatives of the constant distribution

@[simp]

theorem Space.distDeriv_distConst {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin d) (m : M) : (distDeriv μ) (distConst d m) = 0

@[simp]

theorem Space.distGrad_distConst {d : ℕ} (m : ℝ) : distGrad (distConst d m) = 0

@[simp]

theorem Space.distDiv_distConst {d : ℕ} (m : EuclideanSpace ℝ (Fin d)) : distDiv (distConst d m) = 0

@[simp]

theorem Space.distCurl_distConst (m : EuclideanSpace ℝ (Fin 3)) : distCurl (distConst 3 m) = 0