Physlib

Physlib.SpaceAndTime.Space.SmoothFunctions

Smooth real-valued functions on space

`Space.cmap` bundles a smooth real-valued function on `Space d`, given as a plain function together with a `ContDiff` proof, into the space of bundled smooth maps `C^⊤⟮𝓘(ℝ, Space d), Space d; 𝓘(ℝ, ℝ), ℝ⟯`. Such bundled maps are, for instance, the test functions on which the mass distribution of a rigid body acts.

2 declarations

definition

Bundled smooth map f:Space d→Rf: \text{Space } d \to \mathbb{R}

For a given dimension d∈Nd \in \mathbb{N}, let f:Space d→Rf: \text{Space } d \to \mathbb{R} be a real-valued function and hfh_f be a proof that ff is infinitely differentiable (C∞C^\infty). The definition `Space.cmap` bundles ff and hfh_f into an element of the space of bundled smooth maps C∞(Space d,R)C^\infty(\text{Space } d, \mathbb{R}). In this context, Space d\text{Space } d and R\mathbb{R} are treated as smooth manifolds equipped with their standard real model structures.

theorem

cmap(f,hf)(y)=f(y)\text{cmap}(f, h_f)(y) = f(y)

For any dimension d∈Nd \in \mathbb{N}, a real-valued function f:Space d→Rf : \text{Space } d \to \mathbb{R}, and a proof hfh_f that ff is infinitely differentiable (C∞C^\infty), the evaluation of the bundled smooth map cmap(f,hf)\text{cmap}(f, h_f) at a point y∈Space dy \in \text{Space } d is equal to the function value f(y)f(y).