LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Diagonal extraction of a converging Fourier subsequence from high-norm bounds and the tail estimate

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $s > 5 / 2$ and $T > 0$ , and for each $N \geq 1$ let $u_{N} : [0, T] \to H^{s} (T^{3}; R^{3})$ be a field-valued curve with the following properties:

(a) for every $t \in [0, T]$ the coefficients of $u_{N} (t)$ are supported in $∣ k ∣_{\infty} \leq N$ ; (b) for every real $m \geq s$ there is $B_{m} < + \infty$ with $\sup_{N \geq 1} \sup_{0 \leq t \leq T} ∥ u_{N} (t) ∥_{H^{m}} \leq B_{m}$ ; (c) each $u_{N}$ is differentiable into $H^{m - 2}$ for every $m \geq s$ and there are $B_{m}^{'} < + \infty$ with $\sup_{N \geq 1} \sup_{0 \leq t \leq T} ∥ u_{N}^{'} (t) ∥_{H^{m - 2}} \leq B_{m}^{'}$ .

Then there are a subsequence $(N_{j})$ and a field $u : [0, T] \to H^{m}$ for every $m \geq s$ , denoted $u \in ⋂_{m \geq s} C ([0, T], H^{m})$ , such that:

$u_{N_{j}} \to u$ in $C ([0, T], H^{m - 1})$ for every real $m \geq s + 1$ (i.e. $\sup_{0 \leq t \leq T} ∥ u_{N_{j}} (t) - u (t) ∥_{H^{m - 1}} \to 0$ );
$\sup_{0 \leq t \leq T} ∥ u (t) ∥_{H^{m}} \leq B_{m}$ for every $m \geq s$ ;
$u (t)$ is real for every $t$ and is divergence-free whenever every $u_{N} (t)$ is divergence-free, and $\hat{u_{N_{j}} (t)} (k) \to \hat{u} (t) (k)$ for every $k$ and every $t$ , the convergence being uniform in $t$ on every finite set of frequencies;
if in addition $u_{N} (0) \to v$ in $H^{m}$ for every $m \geq s$ , then $u (0) = v$ .

Facts & Assumptions

Given: The sequence $(u_{N})$ with properties (a)-(c), the weights $w_{k} \geq \max (1, 2 π ∣ k ∣_{\infty})$ of Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection, and the coefficient convention $∥ v ∥_{H^{m}}^{2} = \sum_{k} w_{k}^{2 m} ∣ \hat{v} (k) ∣_{2}^{2}$ .

[F1]

For every finite $K$ the set of coefficient vectors $(\hat{v} (k))_{∣ k ∣_{\infty} \leq K} \in C^{3 M_{K}}$ , $M_{K} = # {∣ k ∣_{\infty} \leq K}$ , is in bijection with $R^{6 M_{K}}$ ; a bounded sequence in $R^{6 M_{K}}$ has a convergent subsequence (For $n \geq 1$ every bounded sequence in $R^{n}$ has a convergent subsequence).

[F2]

For $m \geq s > 5 / 2$ , $m - 2 > 0$ and the coefficient functional satisfies $∣ \hat{v} (k) ∣_{2} \leq ∥ v ∥_{H^{m - 2}}$ , since $w_{k} \geq 1$ . Thus $t \mapsto \hat{u_{N}} (k, t)$ is differentiable with derivative bounded by $B_{m}'$ . For $t < t + h$ in $[0, T]$ , apply the real mean-value theorem (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ) to the scalar product of this six-real-coordinate curve with the unit vector in the direction of its endpoint difference (or use zero difference directly). This gives $∣ \hat{u_{N}} (k, t + h) - \hat{u_{N}} (k, t) ∣_{2} \leq ∣ h ∣ B_{m}' \leq ∣ h ∣^{1 / 2} T^{1 / 2} B_{m}'$ because $∣ h ∣ \leq T$ . No continuity or integrability of the derivative is assumed for this argument (Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection).

[F3]

The tail estimate: for every $m$ and every $v \in H^{m}$ , $\sum_{∣ k ∣_{\infty} > K} w_{k}^{2 (m - 1)} ∣ \hat{v} (k) ∣_{2}^{2} \leq (2 π (K + 1))^{- 2} ∥ v ∥_{H^{m}}^{2}$ (Lattice ball and shell counts and weight sums on the frequency lattice, claim 5).

[F4]

The dyadic time set $D = {k T / 2^{n} : n \in N, 0 \leq k \leq 2^{n}}$ is countable and dense in $[0, T]$ : it is the union over $n$ of the finite sets $D_{n} = {k T / 2^{n} : 0 \leq k \leq 2^{n}}$ (Countable unions of at most countable sets, assuming ${A C}_{ω}$ , Finite, countably infinite, countable, uncountable), and for $t \in [0, T]$ and $δ > 0$ one has $∣ t - k T / 2^{n} ∣ \leq T / 2^{n} < δ$ for $n$ large and $k : = ⌊ 2^{n} t / T ⌋$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

[F5]

If a sequence of vectors in a finite-dimensional real normed space converges for each member of a finite set of coordinates, then it converges in the norm; the relations $\hat{u} (- k) = \overline{\hat{u} (k)}$ and $k \cdot \hat{u} (k) = 0$ are preserved by coefficientwise limits (Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection, For $n \geq 1$ every bounded sequence in $R^{n}$ has a convergent subsequence).

Proof

technique · diagonal; extract a subsequence converging at all dyadic times on every finite frequency set, upgrade to uniform convergence in time by the equicontinuity from (c), and control all remaining frequencies by the tail estimate

Given: The sequence $(u_{N})$ , the bounds $B_{m}, B_{m}^{'}$ and the facts [F1]-[F5].

1.1F1F4

Enumerate the countable set of pairs $(k, q)$ , $k \in Z^{3}$ , $q \in D$ , using [F4]. Each real coordinate sequence of $\hat{u_{N}} (k, q)$ is bounded by (b). A bounded real sequence has a deterministically specified convergent subsequence: start with the integer $M \geq 1$ least such that every value lies in $[- M, M]$ ; repeatedly bisect the current closed interval and retain the left half if it contains infinitely many terms, otherwise the right half. At each stage select the least later index whose value belongs to the retained interval. The resulting subsequence is Cauchy because the interval lengths tend to zero, hence converges. Apply this specified rule successively to the six real coordinates of each vector and to each enumerated pair, nesting the infinite index sets. The diagonal index $N_{j}$ is the least member of the $j$ th retained index set larger than $N_{j - 1}$ . For every fixed pair its tail is a subsequence of the corresponding retained sequence and hence converges. This supplies convergence on each finite frequency block at every dyadic time; no dependent selection principle is used.

2.1step 1.1F2F4

For each $k$ and each $t \in [0, T]$ the sequence $(\hat{u_{N_{j}}} (k, t))_{j}$ is Cauchy: given $ϵ > 0$ , pick a dyadic time $q$ with $∣ t - q ∣ \leq δ$ where $∣ h ∣^{1 / 2} T^{1 / 2} B_{s}^{'} < ϵ / 3$ whenever $∣ h ∣ \leq δ$ (possible by the density in [F4]), and then $j, i$ large with $∣ \hat{u_{N_{j}}} (k, q) - \hat{u_{N_{i}}} (k, q) ∣ < ϵ / 3$ ; by the equicontinuity estimate [F2] applied with $m = s$ , $∣ \hat{u_{N_{j}}} (k, t) - \hat{u_{N_{j}}} (k, q) ∣ < ϵ / 3$ and likewise for $N_{i}$ , so the three terms sum to less than $ϵ$ . Hence $\hat{u} (k, t) : = \lim_{j} \hat{u_{N_{j}}} (k, t)$ exists; moreover the convergence is uniform in $t$ on each finite frequency set, because the same finite $δ$ -net of dyadic times can be chosen independently of $j$ and $t$ .

3.1step 2.1F3given

Define $u (t)$ to be the coefficient family $k \mapsto \hat{u} (k, t)$ . For each $m \geq s + 1$ and each finite $K$ , the uniform convergence of step 2.1 and the bound (b) give $\sum_{∣ k ∣_{\infty} \leq K} w_{k}^{2 (m - 1)} ∣ \hat{u} (k, t) ∣^{2} \leq B_{m}^{2}$ for every $t$ ; the tail beyond $K$ is bounded by $(2 π (K + 1))^{- 2} B_{m}^{2}$ by [F3] applied to the $u_{N}$ and passing to the limit in each coefficient. Given $ϵ > 0$ , choose $K$ with $2 B_{m} (2 π (K + 1))^{- 1} < ϵ$ ; then for large $j$ , $∥ u_{N_{j}} (t) - u (t) ∥_{H^{m - 1}} \leq ϵ$ uniformly in $t$ : the finite part converges uniformly by step 2.1 and both tails are small by [F3]. This proves the convergence of claim 1 and, taking the supremum over finite $K$ in the bound, also claim 2 (with $m$ in place of $m - 1$ ). To verify the claimed continuity, for each order $p \geq s$ hypothesis (c) at order $p + 2$ makes every $u_{N}$ differentiable, hence continuous, into $H^{p}$ . Applying the uniform convergence just proved at order $m = p + 1$ shows that $u$ is continuous into $H^{p}$ as a uniform limit. The norm bound at order $p$ follows directly by passing each finite weighted coefficient sum at that order to the limit in (b).

4.1step 3.1F5∎

Realness is preserved under limits by [F5]; if the approximants are divergence-free, their equations $k \cdot \hat{u_{N}} (k, t) = 0$ pass to the limit as well, and the initial condition follows by applying the same convergence statement at $t = 0$ ; this gives claims 3 and 4.

Remarks

The proof chooses subsequences only countably often, which is why ${A C}_{ω}$ and not full choice is assumed. No Arzelà-Ascoli theorem is invoked; the compactness comes from the explicit equicontinuity in time and the finite-dimensional Bolzano-Weierstrass theorem in each finite coefficient block.
The support condition (a) is not used in the extraction except through the fact that the bounds $B_{m}$ are uniform in $N$ ; it is the property that will make the extracted limit a solution of the truncated equations in the main theorem.

Diagonal extraction of a converging Fourier subsequence from high-norm bounds and the tail estimate

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources