Physlib

Physlib.SpaceAndTime.Space.Derivatives.Iterated

Iterated derivatives on `Space d`

i. Overview

This module defines iterated coordinate derivatives on `Space d` indexed by multi-indices.

The implementation is intentionally modest. A multi-index is first expanded into a canonical list of coordinate directions, and the iterated derivative is then defined by repeated application of `Space.deriv` along that list.

ii. Key results

- `Space.iteratedDeriv` : iterated coordinate derivatives on `Space d`. - `∂^[I] f` : notation for the iterated derivative indexed by the multi-index `I`. - `Space.iteratedDeriv_add`, `Space.iteratedDeriv_const_smul` : algebraic compatibility for smooth scalar-valued functions. - `Space.iteratedDeriv_contDiff` : smooth scalar-valued functions remain smooth after iterated coordinate differentiation. - `Space.tsupport_iteratedDeriv_subset` : the support of an iterated spatial derivative is contained in that of the original function.

iii. Table of contents

  • A. Iterated derivatives on `Space d`
  • B. Algebraic and regularity lemmas
  • C. Support lemmas

iv. References

A. Iterated derivatives on `Space d`

12 declarations

definition

Iterated coordinate derivative ∂[I]f\partial^{[I]} f

Given a natural number dd, a multi-index I=(I0,I1,…,Id−1)∈NdI = (I_0, I_1, \dots, I_{d-1}) \in \mathbb{N}^d, and a function f:Space d→Mf: \text{Space } d \to M mapping into a real topological vector space MM, the iterated coordinate derivative ∂[I]f\partial^{[I]} f is the function obtained by repeatedly applying the partial derivative operator ∂μ\partial_\mu (defined as `Space.deriv`) for each coordinate index μ\mu in the canonical list associated with II. This corresponds to the standard partial derivative of ff of order ∣I∣|I| indexed by the multi-index II, denoted as: ∂[I]f=∂∣I∣f∂x0I0∂x1I1⋯∂xd−1Id−1\partial^{[I]} f = \frac{\partial^{|I|} f}{\partial x_0^{I_0} \partial x_1^{I_1} \cdots \partial x_{d-1}^{I_{d-1}}}

definition

Notation for the iterated derivative ∂[I]\partial^{[I]}

The notation ∂[I]\partial^{[I]} denotes the iterated coordinate derivative operator indexed by a multi-index II. For a function f:Space d→Mf: \text{Space } d \to M, where MM is a module over R\mathbb{R}, ∂[I]f\partial^{[I]} f represents the repeated application of the coordinate derivative `Space.deriv` along the directions specified by the multi-index II.

theorem

∂[0]f=f\partial^{[0]} f = f

Let MM be a real topological vector space and dd be a natural number. For any function f:Space d→Mf: \text{Space } d \to M, the iterated coordinate derivative with respect to the zero multi-index 00 is the function itself: ∂[0]f=f\partial^{[0]} f = f

theorem

∂[I+e0]f=∂0(∂[I]f)\partial^{[I + e_0]} f = \partial_0 (\partial^{[I]} f)

Let MM be a real topological vector space and f:Space(d+1)→Mf: \text{Space}(d+1) \to M be a function. For any multi-index I=(I0,…,Id)∈Nd+1I = (I_0, \dots, I_d) \in \mathbb{N}^{d+1}, the iterated coordinate derivative of ff indexed by the multi-index incremented at the 00-th coordinate is given by: ∂[I+e0]f=∂0(∂[I]f)\partial^{[I + e_0]} f = \partial_0 (\partial^{[I]} f) where I+e0I + e_0 denotes the multi-index (I0+1,I1,…,Id)(I_0 + 1, I_1, \dots, I_d), ∂[I]f\partial^{[I]} f is the iterated coordinate derivative of ff with respect to II, and ∂0\partial_0 is the partial derivative with respect to the 00-th coordinate.

theorem

∂[ei]f=∂if\partial^{[e_i]} f = \partial_i f

Let f:Space d→Mf: \text{Space } d \to M be a function mapping into a real topological vector space MM, and let i∈{0,…,d−1}i \in \{0, \dots, d-1\} be a coordinate index. Let eie_i denote the unit multi-index with 11 at the ii-th position and 00 elsewhere (defined as the increment of the zero multi-index at ii). Then the iterated coordinate derivative ∂[ei]f\partial^{[e_i]} f is equal to the spatial derivative in the ii-th direction ∂if\partial_i f.

theorem

∂[I](f+g)=∂[I]f+∂[I]g\partial^{[I]} (f + g) = \partial^{[I]} f + \partial^{[I]} g

Let dd be a natural number and I∈NdI \in \mathbb{N}^d be a multi-index of dimension dd. For any two infinitely differentiable (smooth) functions f,g:Space d→Rf, g: \text{Space } d \to \mathbb{R}, the iterated coordinate derivative of their sum is equal to the sum of their individual iterated coordinate derivatives: ∂[I](f+g)=∂[I]f+∂[I]g\partial^{[I]} (f + g) = \partial^{[I]} f + \partial^{[I]} g

theorem

∂[I](c⋅f)=c⋅∂[I]f\partial^{[I]} (c \cdot f) = c \cdot \partial^{[I]} f for smooth functions

Let dd be a natural number and I=(I0,I1,…,Id−1)∈NdI = (I_0, I_1, \dots, I_{d-1}) \in \mathbb{N}^d be a multi-index. For any real constant c∈Rc \in \mathbb{R} and any smooth function f:Space d→Rf: \text{Space } d \to \mathbb{R} (i.e., f∈C∞f \in C^\infty), the iterated coordinate derivative of the scalar multiple c⋅fc \cdot f satisfies: ∂[I](c⋅f)=c⋅∂[I]f\partial^{[I]} (c \cdot f) = c \cdot \partial^{[I]} f where ∂[I]\partial^{[I]} denotes the partial derivative operator ∂∣I∣∂x0I0∂x1I1⋯∂xd−1Id−1\frac{\partial^{|I|}}{\partial x_0^{I_0} \partial x_1^{I_1} \cdots \partial x_{d-1}^{I_{d-1}}}.

theorem

Iterated derivatives of smooth functions are smooth

Let dd be a natural number and Space d\text{Space } d be the dd-dimensional real inner product space. For any multi-index I∈NdI \in \mathbb{N}^d and any smooth scalar-valued function f:Space d→Rf: \text{Space } d \to \mathbb{R} (i.e., ff is C∞C^\infty), the iterated coordinate derivative ∂[I]f\partial^{[I]} f is also a smooth function.

theorem

tsupport⁡(∂if)⊆tsupport⁡(f)\operatorname{tsupport}(\partial_i f) \subseteq \operatorname{tsupport}(f)

Let f:Space d→Rf: \text{Space } d \to \mathbb{R} be a function and i∈{0,…,d−1}i \in \{0, \dots, d-1\} be a coordinate index. Let ∂if\partial_i f denote the spatial derivative of ff in the ii-th coordinate direction. Then the topological support of the spatial derivative is contained in the topological support of the original function: tsupport⁡(∂if)⊆tsupport⁡(f) \operatorname{tsupport}(\partial_i f) \subseteq \operatorname{tsupport}(f)

theorem

∂i\partial_i and ∂[I]\partial^{[I]} commute for smooth functions

Let f:Space d→Rf: \text{Space } d \to \mathbb{R} be an infinitely differentiable (smooth) scalar-valued function. For any coordinate index i∈{0,…,d−1}i \in \{0, \dots, d-1\} and any multi-index I∈NdI \in \mathbb{N}^d, the spatial derivative ∂i\partial_i commutes with the iterated multi-index derivative ∂[I]\partial^{[I]}. That is, ∂i(∂[I]f)=∂[I](∂if) \partial_i (\partial^{[I]} f) = \partial^{[I]} (\partial_i f) where ∂i\partial_i is the partial derivative with respect to the ii-th coordinate and ∂[I]\partial^{[I]} is the iterated coordinate derivative defined by the multi-index II.

theorem

supp(∂[I]f)⊆supp(f)\text{supp}(\partial^{[I]} f) \subseteq \text{supp}(f)

Let dd be a natural number and I=(I0,I1,…,Id−1)∈NdI = (I_0, I_1, \dots, I_{d-1}) \in \mathbb{N}^d be a multi-index. For any real-valued function f:Space d→Rf: \text{Space } d \to \mathbb{R}, the topological support of its iterated coordinate derivative ∂[I]f\partial^{[I]} f, defined as ∂[I]f=∂∣I∣f∂x0I0∂x1I1⋯∂xd−1Id−1,\partial^{[I]} f = \frac{\partial^{|I|} f}{\partial x_0^{I_0} \partial x_1^{I_1} \cdots \partial x_{d-1}^{I_{d-1}}}, is a subset of the topological support of ff. That is, supp(∂[I]f)⊆supp(f).\text{supp}(\partial^{[I]} f) \subseteq \text{supp}(f).

theorem

∂[I]f(x)=0\partial^{[I]} f(x) = 0 for x∉supp(f)x \notin \text{supp}(f)

Let dd be a natural number and I=(I0,I1,…,Id−1)∈NdI = (I_0, I_1, \dots, I_{d-1}) \in \mathbb{N}^d be a multi-index. For any real-valued function f:Space d→Rf: \text{Space } d \to \mathbb{R} and any point x∈Space dx \in \text{Space } d, if xx is not in the topological support of ff (denoted supp(f)\text{supp}(f)), then the iterated coordinate derivative ∂[I]f\partial^{[I]} f vanishes at xx: ∂[I]f(x)=0\partial^{[I]} f(x) = 0 where ∂[I]f\partial^{[I]} f is defined as: ∂[I]f=∂∣I∣f∂x0I0∂x1I1⋯∂xd−1Id−1\partial^{[I]} f = \frac{\partial^{|I|} f}{\partial x_0^{I_0} \partial x_1^{I_1} \cdots \partial x_{d-1}^{I_{d-1}}}