Physlib.SpaceAndTime.Time.Derivatives

Given a function $f : \text{Time} \to M$, where $M$ is a topological vector space over $\mathbb{R}$ (specifically, an additive commutative group and a module over $\mathbb{R}$ with a topology), the time derivative of $f$ is a function from $\text{Time}$ to $M$. For each $t \in \text{Time}$, the value of the derivative is defined as the Fréchet derivative of $f$ at $t$ evaluated at the unit element $1 \in \text{Time}$.

The symbol $\partial_t$ is a notation for the time derivative operator `deriv`. For a function $f : \text{Time} \to M$, where $M$ is a topological vector space over $\mathbb{R}$, $\partial_t f$ denotes the derivative of $f$ with respect to time.

Let $M$ be a topological vector space over $\mathbb{R}$ (specifically, an additive commutative group and a module over $\mathbb{R}$ with a topology). For any function $f : \text{Time} \to M$ and any time $t \in \text{Time}$, the time derivative of $f$ at $t$, denoted by $\text{Time.deriv } f(t)$, is equal to the Fréchet derivative of $f$ at $t$ evaluated at the unit element $1 \in \text{Time}$.

Let $f : \text{Time} \to \mathbb{R}^d$ be a differentiable function and $k \in \mathbb{R}$ be a scalar. For any time $t \in \text{Time}$, the time derivative of the scaled function $k \cdot f$ is equal to the scalar $k$ multiplied by the time derivative of $f$, that is, $\partial_t (k \cdot f(t)) = k \cdot \partial_t f(t)$.

Let $M$ be a normed vector space over the real numbers $\mathbb{R}$. For any function $f : \text{Time} \to M$ and any time $t \in \text{Time}$, the time derivative of the negative of $f$ at $t$ is equal to the negative of the time derivative of $f$ at $t$, expressed as $\partial_t (-f)(t) = -\partial_t f(t)$.

Let $M$ be a normed vector space over the real numbers $\mathbb{R}$. For any constant element $m \in M$, the time derivative of the constant function $f(t) = m$ at any time $t$ is equal to zero, that is, $\partial_t (\lambda t, m) = 0$.

Let $M$ be a real normed space. If a function $f : \text{Time} \to M$ is of class $C^\infty$, then its time derivative $\partial_t f : \text{Time} \to M$ is differentiable.

Let $M$ be a real normed space. If a function $f : \text{Time} \to M$ is of class $C^\infty$, then its time derivative $\partial_t f$ is also of class $C^\infty$.

Let $M$ be a real normed space and $f : \text{Time} \times \text{Space } d \to M$ be a function. If the uncurried function $(t, x) \mapsto f(t, x)$ is of class $C^{n+1}$, then for any fixed $t \in \text{Time}$, the function $x \mapsto \frac{\partial f}{\partial t}(t, x)$ is of class $C^n$ on $\text{Space } d$, where $\frac{\partial f}{\partial t}$ denotes the time derivative.

Let $f : \text{Time} \to \mathbb{R}^n$ be a function from time into an $n$-dimensional Euclidean space. If for every coordinate index $i$, the component function $t \mapsto f(t)_i$ is differentiable over $\mathbb{R}$, then the function $f$ is differentiable over $\mathbb{R}$.

Let $f : \text{Time} \to \mathbb{R}^n$ be a differentiable function from time into an $n$-dimensional Euclidean space. For any coordinate index $\mu$ and any time $t \in \text{Time}$, the derivative of the $\mu$-th component function $t \mapsto f(t)_\mu$ is equal to the $\mu$-th component of the derivative of $f$. That is, $$\frac{d}{dt}(f(t)_\mu) = \left( \frac{df}{dt}(t) \right)_\mu$$

Let $f: \text{Time} \to \mathbb{R}^n$ be a differentiable function into an $n$-dimensional Euclidean space. For any coordinate index $\mu$ and time values $t, \Delta t \in \text{Time}$, the Frechet derivative of the component function $t \mapsto f(t)_\mu$ at $t$ applied to the increment $\Delta t$ is equal to the $\mu$-th component of the Frechet derivative of $f$ at $t$ applied to $\Delta t$. That is, $$D(f_\mu)(t)(\Delta t) = (Df(t)(\Delta t))_\mu$$ where $D$ denotes the Frechet derivative over the real numbers.

Let $f : \text{Time} \to \text{Vector}_d$ be a differentiable function from the time domain to the space of $d$-dimensional Lorentz vectors. For any time $t \in \text{Time}$ and any coordinate index $i \in \text{Fin } 1 \oplus \text{Fin } d$, the time derivative of the $i$-th component function $t \mapsto f(t)_i$ is equal to the $i$-th component of the time derivative of $f$ at $t$. That is, $$\frac{d}{dt} (f(t)_i) = \left( \frac{df}{dt}(t) \right)_i$$ where $\frac{d}{dt}$ denotes the time derivative `Time.deriv`.

Let $c, g : \text{Time} \to \mathbb{R}$ be real-valued functions of time. If $c$ and $g$ are differentiable at $t \in \text{Time}$ and $g(t) \neq 0$, then the time derivative of their quotient at $t$ is given by: $$\partial_t \left( \frac{c}{g} \right)(t) = \frac{(\partial_t c)(t) \cdot g(t) - c(t) \cdot (\partial_t g)(t)}{(g(t))^2}$$ where $\partial_t$ denotes the time derivative operator `Time.deriv`.

Let $M$ be a real normed vector space and $s$ be a finite set of indices. If for every $i \in s$, the function $a_i : \text{Time} \to M$ is differentiable at a time $t$, then the time derivative of the sum of these functions at $t$ is equal to the sum of their individual time derivatives at $t$: $$\frac{d}{dt} \left( \sum_{i \in s} a_i(t) \right) = \sum_{i \in s} \frac{d}{dt} a_i(t)$$ where $\frac{d}{dt}$ denotes the time derivative (defined as the Fréchet derivative at $t$ evaluated at the unit time).

The function $\text{Time.val} : \text{Time} \to \mathbb{R}$, which maps a time value to its underlying real-number representation, is $n$-times continuously differentiable for any $n \in \mathbb{N} \cup \{\infty\}$.

Let $d$ be a natural number and $f: \text{Time} \to \text{Space } d$ be a differentiable function. For any $t \in \text{Time}$ and index $i \in \{0, \dots, d-1\}$, the derivative of the $i$-th component function $s \mapsto f(s)_i$ at time $t$ is equal to the $i$-th component of the derivative of $f$ at $t$. That is: $$\text{deriv}\left(\lambda s, f(s)_i\right)(t) = \left(\text{deriv } f(t)\right)_i$$