Fefferman's admissible initial data are exactly the divergence-free Schwartz functions

Read-back of isInitialData_iff_schwartz.

Fix a natural number $n \ge 0$ (implicit, so the statement is asserted for every $n$, including $n = 0$) and write $V = \mathbb{R}^n$ for Euclidean $n$-space with its standard Euclidean ($\ell^2$) norm $\|\cdot\|$ and standard basis vectors $e_1,\dots,e_n$ (the $i$-th one has a $1$ in coordinate $i$ and $0$ elsewhere). Let $u_0 : V \to V$ be an arbitrary function — no hypothesis whatsoever is placed on $u_0$; in particular it need not be continuous or differentiable. Throughout, $Du_0(x) : V \to V$ denotes Mathlib's Fréchet derivative of $u_0$ at $x$, which is a total operation: if $u_0$ is not differentiable at $x$ it returns the zero linear map. Likewise $D^k u_0(x)$ denotes the $k$-th iterated Fréchet derivative at $x$, a continuous $k$-multilinear map $V^k \to V$ with $D^0 u_0(x)$ being just the vector $u_0(x)$ (viewed as a $0$-multilinear map, so $\|D^0 u_0(x)\| = \|u_0(x)\|$), and $\|D^k u_0(x)\|$ its operator norm; for non-smooth $u_0$ these too take whatever "junk" values the total definitions assign (built from the zero-default derivative). The custom divergence is

the sum over $i$ of the $i$-th coordinate of the directional derivative of $u_0$ at $x$ in direction $e_i$; wherever $u_0$ fails to be differentiable this is the empty-map value $0$, and when $n=0$ it is an empty sum, hence $0$.

The theorem asserts, for every such $n$ and $u_0$, the biconditional

Left-hand side, unfolded. $\mathrm{IsInitialData}(u_0)$ is the conjunction of exactly three conditions:

1. (smooth) $u_0$ is $C^\infty$ on all of $V$ in the Fréchet sense (Mathlib's ContDiff ℝ ∞, with $\infty$ meaning infinitely differentiable, not analytic);
2. (divFree) for every $x \in V$, $\operatorname{div} u_0(x) = 0$, with $\operatorname{div}$ as defined above;
3. (decay) for every pair of natural numbers $k, K \ge 0$ there exists a real number $C$ (depending on $k$ and $K$ but not on $x$; no sign restriction on $C$ is imposed, though the left side of the inequality is $\ge 0$) such that for every $x \in V$,

Here $k$ is the derivative order and $K$ the weight exponent; the case $k = 0$ reads $(1+\|x\|)^K \|u_0(x)\| \le C$, and the case $K = 0$ says each $\|D^k u_0\|$ is bounded on $V$. The inequality is non-strict ($\le$).

Right-hand side, unfolded. The first conjunct is literally the same statement as condition 2 above: $\operatorname{div} u_0(x) = 0$ for every $x$. The second conjunct asserts the existence (mere existence, not uniqueness) of an element $\varphi$ of Mathlib's Schwartz space $\mathcal{S}(V;V)$ whose underlying function coincides with $u_0$ pointwise, i.e. $\varphi(x) = u_0(x)$ for all $x \in V$. A Schwartz map $\varphi : V \to V$ in Mathlib is a function together with proofs of:

• (smooth') $\varphi$ is $C^\infty$ on $V$ (the same ContDiff ℝ ∞ predicate as in condition 1);
• (decay') for every pair of natural numbers $k, m \ge 0$ there exists a real $C$ such that for every $x \in V$,

where now $k$ is the weight exponent and $m$ the derivative order, and the weight is $\|x\|^k$ rather than $(1+\|x\|)^k$.

So the biconditional says: $u_0$ is smooth, divergence-free (in the custom sense), and satisfies the $(1+\|x\|)^K$-weighted bounds on all iterated derivatives, if and only if $u_0$ is divergence-free (same custom sense) and is the underlying function of some Schwartz map, i.e. is smooth and satisfies the $\|x\|^k$-weighted bounds on all iterated derivatives.

Edge and degenerate cases made explicit. (i) When $n = 0$, $V$ is the one-point space $\{0\}$, every $u_0$ is constant and smooth, $\operatorname{div} u_0 \equiv 0$ as an empty sum, $\|u_0(0)\| = 0$ since the codomain is the zero space, and all iterated derivatives vanish, so both sides hold for every $u_0$ and the biconditional is trivially true there. (ii) The divergence condition appears identically on both sides; because the Fréchet derivative defaults to $0$ at points of non-differentiability, $\operatorname{div} u_0(x) = 0$ holds automatically at any such point, so this condition by itself constrains $u_0$ only where $u_0$ is differentiable. (iii) The decay conditions on both sides are stated using total operations, so they are meaningful (and evaluate to something) even for non-smooth $u_0$, but each side also independently demands smoothness, so junk derivative values only matter for functions that fail the smoothness clause anyway. (iv) Neither side is vacuous: the theorem carries no hypotheses beyond the choice of $n$ and $u_0$, and the zero function $u_0 \equiv 0$ satisfies both sides, while e.g. a non-smooth $u_0$ satisfies neither; the statement is a claim about every function $V \to V$ for every $n$. (v) The existential on the right is $\exists$, not $\exists!$; the equation $\varphi = u_0$ is equality of functions $V \to V$ (equivalently, pointwise equality at every $x$), and the constants $C$ in both decay clauses may be any real numbers, chosen after $k$ and the weight exponent but before $x$.