Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.SpaceAndTime.Space.Derivatives.CurlThe 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
@[expose] public sectionA. The definition of the constant distribution
B. Derivatives of the constant distribution
@[simp]
lemma distDeriv_distConst {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
(μ : Fin d) (m : M) :
distDeriv μ (distConst d m) = 0 := M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin dm:M⊢ (distDeriv μ) (distConst d m) = 0
All goals completed! 🐙@[simp]
lemma distGrad_distConst {d} (m : ℝ) :
distGrad (distConst d m) = 0 := d:ℕm:ℝ⊢ ∇ᵈ (distConst d m) = 0
All goals completed! 🐙@[simp]
lemma distDiv_distConst {d} (m : EuclideanSpace ℝ (Fin d)) :
distDiv (distConst d m) = 0 := d:ℕm:EuclideanSpace ℝ (Fin d)⊢ distDiv (distConst d m) = 0
All goals completed! 🐙@[simp]
lemma distCurl_distConst (m : EuclideanSpace ℝ (Fin 3)) :
distCurl (distConst 3 m) = 0 := m:EuclideanSpace ℝ (Fin 3)⊢ distCurl (distConst 3 m) = 0
All goals completed! 🐙