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.

The Galerkin coefficient system: finite-dimensional invariance, local Lipschitz property, and the unique maximal approximation on the torus

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), used through the Fourier-coefficient suppliers. Fix $N \geq 1$ , a real viscosity parameter $ν \geq 0$ and a real exponent $s > 3 / 2$ . Work in the notation of Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection: $H^{s} = H^{s} (T^{3}; R^{3})$ with coefficients $\hat{u} (k)$ , weights $w_{k}$ , Leray projection $P$ , differential operators $\partial_{j}, Δ$ and divergence-free subspace $H_{σ}^{s}$ .

Definitions. For a coefficient family $c$ let $(P_{N} c) (k) : = c (k)$ if $∣ k ∣_{\infty} \leq N$ and $(P_{N} c) (k) : = 0$ otherwise (\emph{Fourier truncation}); let $X_{N} : = {u \in H^{0} : \hat{u} (k) = 0 for ∣ k ∣_{\infty} > N, k \cdot \hat{u} (k) = 0 \forall k, \hat{u} (- k) = \overline{\hat{u} (k)} \forall k}$ be the space of real divergence-free trigonometric-polynomial fields of frequency at most $N$ , and define the Galerkin field $F_{N} : X_{N} ⟶ H^{0}, F_{N} (u) : = - P_{N} P ((u \cdot \nabla) u) + ν Δ u .$

Then:

$X_{N}$ is a finite-dimensional real-linear subspace of $H^{s}$ for every $s \in R$ , $P_{N}$ restricted to the real divergence-free subspace $H_{σ}^{s}$ is the orthogonal projection onto $X_{N}$ for the $H^{s}$ inner product and $∥ P_{N} u ∥_{H^{s}} \leq ∥ u ∥_{H^{s}}$ ; moreover $F_{N}$ maps $X_{N}$ into $X_{N}$ , and $\int_{T^{3}} F_{N} (u) d x = 0$ and $F_{N} (P_{N} u) = F_{N} (u)$ for $u \in X_{N}$ .
Local Lipschitz property. For every $R > 0$ there is $L_{N} (R) < + \infty$ such that $∥ F_{N} (u) - F_{N} (v) ∥_{H^{s}} \leq L_{N} (R) ∥ u - v ∥_{H^{s}}$ whenever $u, v \in X_{N}$ with $∥ u ∥_{H^{s}}, ∥ v ∥_{H^{s}} \leq R$ ; the proof exhibits $L_{N} (R) = 12 π^{2} ν N^{2} + 6 C_{s} c_{N} R$ with $c_{N} = (1 + 12 π^{2} N^{2})^{1 / 2}$ and $C_{s}$ the product constant of Discrete Young inequality, the Sobolev product bound, and the transport product bound on the torus.
Galerkin IVP. For every $u_{0} \in X_{N}$ the initial value problem $u^{'} (t) = F_{N} (u (t)), u (0) = u_{0}$ has a unique maximal solution $u_{N} : I \to X_{N}$ with open interval $I ∋ 0$ ; if the maximal interval has finite right endpoint $T_{\max} < + \infty$ , then $\lim_{t ↑ T_{\max}} ∥ u_{N} (t) ∥_{H^{s^{'}}} = + \infty$ for every $s^{'} > 3 / 2$ , and conversely if $∥ u_{N} ∥_{H^{s^{'}}} \leq R$ on $[0, T)$ for some $s^{'} > 3 / 2$ with $T < + \infty$ then the solution extends past $T$ . For $u_{0} \in H_{σ}^{0}$ arbitrary, $P_{N} u_{0} \in X_{N}$ and the corresponding solution is written $u_{N} (\cdot; P_{N} u_{0})$ .
Basic bounds. Along the maximal solution: (a) for every real $m > 3 / 2$ , $∥ u_{N}^{'} (t) ∥_{H^{m}} \leq ν ∥ u_{N} (t) ∥_{H^{m + 2}} + 3 C_{m} ∥ u_{N} (t) ∥_{H^{m + 1}}^{2},$ where $C_{m}$ is the product constant of Discrete Young inequality, the Sobolev product bound, and the transport product bound on the torus at order $m$ ; (b) for every real $0 \leq m \leq 2$ , with $c_{N} = (1 + 12 π^{2} N^{2})^{1 / 2}$ and $e_{N} = (1 + 48 π^{2} N^{2})^{1 / 2}$ , $∥ u_{N}^{'} (t) ∥_{H^{m}} \leq 12 π^{2} ν N^{2} ∥ u_{N} (t) ∥_{H^{m}} + 3 C_{s} c_{N} e_{N}^{2} ∥ u_{N} (t) ∥_{H^{s}}^{2};$ (c) $∥ P_{N} u - u ∥_{H^{r}} \leq (2 π (N + 1))^{- 1} ∥ u ∥_{H^{r + 1}}$ for every real $r$ and every $u \in H^{r + 1}$ .

Facts & Assumptions

Given: The finite support $∣ k ∣_{\infty} \leq N$ , the weight family with $w_{k} \geq \max (1, 2 π ∣ k ∣_{\infty}, 2 π ∣ k ∣_{j})$ , and the operators of Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection.

[F1]

For a finitely supported family with $∣ k ∣_{\infty} \leq N$ one has $∥ u ∥_{H^{r + 1}} \leq c_{N} ∥ u ∥_{H^{r}}$ for every real $r$ , and $∥ Δ u ∥_{H^{r}} \leq 12 π^{2} N^{2} ∥ u ∥_{H^{r}}$ , because $w_{k} \leq c_{N} : = (1 + 12 π^{2} N^{2})^{1 / 2}$ and $∣ 2 π k ∣_{2}^{2} \leq 12 π^{2} N^{2}$ on the support, where $∣ k ∣_{2}^{2} \leq 3 N^{2}$ (Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection).

[F2]

For $σ > 3 / 2$ the product bounds $∥ f g ∥_{H^{σ}} \leq C_{σ} ∥ f ∥_{H^{σ}} ∥ g ∥_{H^{σ}}$ and $∥ (f \cdot \nabla) g ∥_{H^{σ}} \leq 3 C_{σ} ∥ f ∥_{H^{σ}} ∥ g ∥_{H^{σ + 1}}$ hold with $C_{σ} = 2^{σ} W_{σ}$ (Discrete Young inequality, the Sobolev product bound, and the transport product bound on the torus, claims 2 and 3); $C_{s}$ denotes this constant at order $s$ .

[F3]

$P$ is an orthogonal projection (self-adjoint, idempotent, norm nonincreasing) in every $H^{s}$ ; $P$ commutes with $Δ$ and $\partial_{j}$ ; $P \nabla f = 0$ ; and $div (P u) = 0$ (Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection).

[F4]

A locally Lipschitz field on an open subset of $R^{n}$ has a unique local solution through every initial point (Picard-Lindelöf local existence and uniqueness for first-order systems), and every initial value problem satisfying the Picard-Lindelof hypotheses has a unique maximal solution whose domain is an open interval containing the initial time (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, Extensions, maximal solutions, maximal intervals, and global solutions).

[F5]

Let $v_{0}, \dots, v_{M - 1}$ be an ordered basis (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis) of the finite-dimensional real vector space $X_{N}$ and $T (a) : = \sum_{i < M} a_{i} v_{i}$ . Then $T$ is a topological isomorphism onto its span (A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space), so there are constants $0 < b \leq B < + \infty$ with $b ∥ a ∥_{1} \leq ∥ T (a) ∥_{H^{s}} \leq B ∥ a ∥_{1}$ for every $a \in R^{M}$ ; the same holds with $∥ \cdot ∥_{H^{s^{'}}}$ in place of $∥ \cdot ∥_{H^{s}}$ for every real $s^{'}$ , with constants $b^{'}, B^{'}$ depending on $s^{'}$ . Moreover $∥ a ∥_{2} \leq ∥ a ∥_{1} \leq \sqrt{M} ∥ a ∥_{2}$ for every $a \in R^{M}$ (The Cauchy-Schwarz inequality for finite sums).

[F6]

For a trigonometric polynomial $W$ on $T^{3}$ one has $\int_{T^{3}} div W d x = 0$ ; for divergence-free $u$ , the $i$ -th component satisfies $\sum_{j = 1}^{3} u_{j} \partial_{j} u_{i} = \sum_{j = 1}^{3} \partial_{j} (u_{j} u_{i})$ , by the product rule and $\sum_{j} \partial_{j} u_{j} = 0$ ; each scalar derivative has zero coefficient at $k = 0$ (Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection, The Fourier basis and Parseval's identity on the finite torus).

[F7]

$∥ P_{N} u - u ∥_{H^{r}} \leq (2 π (N + 1))^{- 1} ∥ u ∥_{H^{r + 1}}$ for $u \in H^{r + 1}$ : the tail sum over $∣ k ∣_{\infty} > N$ is bounded by $(2 π (N + 1))^{- 2}$ times the $H^{r + 1}$ -weighted sum (Lattice ball and shell counts and weight sums on the frequency lattice, claim 5).

[F8]

If $v \in H^{0}$ has Fourier support in $∣ k ∣_{\infty} \leq 2 N$ and $0 \leq m \leq 2$ then $∥ v ∥_{H^{m}} \leq e_{N}^{m} ∥ v ∥_{H^{0}} \leq e_{N}^{2} ∥ v ∥_{H^{0}}$ with $e_{N} : = (1 + 48 π^{2} N^{2})^{1 / 2}$ , because $w_{k} \leq e_{N}$ on that support and $w_{k} \geq 1$ (Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection).

Proof

technique · direct; the finite-dimensional coefficient space carries a polynomial vector field, so Picard-Lindelof supplies the maximal solution, while the invariance and Lipschitz bounds are explicit finite-sum estimates

Given: $N \geq 1$ , $ν \geq 0$ , the space $X_{N}$ , the field $F_{N}$ and the facts [F1]-[F8].

1.1givenF1

$X_{N}$ is a real-linear subspace of the coefficient space: the support condition $∣ k ∣_{\infty} \leq N$ and the two linear conditions $k \cdot \hat{u} (k) = 0$ , $\hat{u} (- k) = \overline{\hat{u} (k)}$ are preserved by sums and real multiples. It is spanned by $P ((Re e_{k}) e_{i})$ and $P ((Im e_{k}) e_{i})$ for $∣ k ∣_{\infty} \leq N$ and standard coordinate vectors $e_{i} \in R^{3}$ : these are real divergence-free polynomials in $X_{N}$ , and applying $P$ to the ordinary finite Fourier expansion of any $u \in X_{N}$ fixes $u$ . Order this finite spanning list, then process it in order, retaining a vector exactly when it is not in the span of the vectors already retained. Induction gives a linearly independent list spanning all processed vectors, hence an ordered basis after the final vector. Thus $X_{N}$ is finite-dimensional, and it is contained in $H^{s}$ for every $s$ because only finitely many coefficients are nonzero. The truncation $P_{N}$ is the orthogonal projection onto the support condition: it commutes with the weights $w_{k}^{2 s}$ , is idempotent and self-adjoint, and $∥ P_{N} u ∥_{H^{s}} \leq ∥ u ∥_{H^{s}}$ .

2.1step 1.1F3F6

$F_{N}$ maps $X_{N}$ into $X_{N}$ : for $u \in X_{N}$ , the field $(u \cdot \nabla) u$ is a trigonometric polynomial with support in $∣ k ∣_{\infty} \leq 2 N$ (a finite convolution of supports), and $P$ , $P_{N}$ and $Δ$ preserve finite support, reality and the divergence-free condition (for $P$ by [F3], for $P_{N}$ and $Δ$ coefficientwise), so $F_{N} (u) \in X_{N}$ . Moreover $\hat{F_{N} (u)} (0) = - \hat{P ((u \cdot \nabla) u)} (0) + ν \hat{Δ u} (0)$ and $\hat{Δ u} (0) = - 4 π^{2} \cdot 0 \cdot \hat{u} (0) = 0$ , while each component of $(u \cdot \nabla) u$ is a sum of scalar derivatives by [F6], each with zero coefficient at $0$ ; hence $\int F_{N} (u) d x = 0$ . Finally $P_{N}$ is the identity on $X_{N}$ , so $F_{N} (P_{N} u) = F_{N} (u)$ for $u \in X_{N}$ .

3.1step 2.1F1F2F3

Local Lipschitz bound. For $u, v \in X_{N}$ put $h : = u - v$ . Then $F_{N} (u) - F_{N} (v) = - P_{N} P ((u \cdot \nabla) h + (h \cdot \nabla) v) + ν Δ h$ . By [F1], $∥ Δ h ∥_{H^{s}} \leq 12 π^{2} N^{2} ∥ h ∥_{H^{s}}$ and $∥ h ∥_{H^{s + 1}} \leq c_{N} ∥ h ∥_{H^{s}}$ ; by [F2], $∥ (u \cdot \nabla) h ∥_{H^{s}} \leq 3 C_{s} ∥ u ∥_{H^{s}} ∥ h ∥_{H^{s + 1}} \leq 3 C_{s} c_{N} ∥ u ∥_{H^{s}} ∥ h ∥_{H^{s}}$ and likewise $∥ (h \cdot \nabla) v ∥_{H^{s}} \leq 3 C_{s} c_{N} ∥ v ∥_{H^{s}} ∥ h ∥_{H^{s}}$ . Since $P$ and $P_{N}$ are norm nonincreasing [F3], $∥ F_{N} (u) - F_{N} (v) ∥_{H^{s}} \leq (12 π^{2} ν N^{2} + 3 C_{s} c_{N} (∥ u ∥_{H^{s}} + ∥ v ∥_{H^{s}})) ∥ h ∥_{H^{s}}$ , which is at most $L_{N} (R) ∥ u - v ∥_{H^{s}}$ with $L_{N} (R) : = 12 π^{2} ν N^{2} + 6 C_{s} c_{N} R$ whenever $∥ u ∥_{H^{s}}, ∥ v ∥_{H^{s}} \leq R$ .

3.2step 2.1F1F8F2F3F7

Derivative bounds. Part (a): for $m > 3 / 2$ , by [F2] and [F3], $∥ F_{N} (u) ∥_{H^{m}} \leq ν ∥ Δ u ∥_{H^{m}} + ∥ (u \cdot \nabla) u ∥_{H^{m}} \leq ν ∥ u ∥_{H^{m + 2}} + 3 C_{m} ∥ u ∥_{H^{m}} ∥ u ∥_{H^{m + 1}} \leq ν ∥ u ∥_{H^{m + 2}} + 3 C_{m} ∥ u ∥_{H^{m + 1}}^{2}$ . Part (b): let $0 \leq m \leq 2$ and $v : = (u \cdot \nabla) u$ , a trigonometric polynomial with support in $∣ k ∣_{\infty} \leq 2 N$ (step 2.1); by [F8], $∥ P_{N} P v ∥_{H^{m}} \leq ∥ v ∥_{H^{m}} \leq e_{N}^{2} ∥ v ∥_{H^{0}}$ , and by [F2] with [F1], $∥ v ∥_{H^{0}} \leq ∥ v ∥_{H^{s}} \leq 3 C_{s} ∥ u ∥_{H^{s}} ∥ u ∥_{H^{s + 1}} \leq 3 C_{s} c_{N} ∥ u ∥_{H^{s}}^{2}$ ; since $∥ Δ u ∥_{H^{m}} \leq 12 π^{2} N^{2} ∥ u ∥_{H^{m}}$ by [F1], adding the two terms gives (b). Part (c) is [F7]. This is claim 4.

4.1step 3.1F4F5

The maximal solution. Fix an ordered basis $v_{0}, \dots, v_{M - 1}$ of $X_{N}$ ( $M : = \dim_{R} X_{N}$ ) and put $T (a) : = \sum_{i < M} a_{i} v_{i}$ , so that $T^{- 1} : X_{N} \to R^{M}$ is well defined. Let $G : = T^{- 1} \circ F_{N} \circ T : R^{M} \to R^{M}$ . For $∥ a ∥_{2}, ∥ a^{'} ∥_{2} \leq ρ$ put $R : = B \sqrt{M} ρ$ , so that $∥ T (a) ∥_{H^{s}}, ∥ T (a^{'}) ∥_{H^{s}} \leq R$ by [F5], and step 3.1 gives $∥ G (a) - G (a^{'}) ∥_{2} \leq ∥ G (a) - G (a^{'}) ∥_{1} \leq b^{- 1} ∥ F_{N} (T a) - F_{N} (T a^{'}) ∥_{H^{s}} \leq b^{- 1} L_{N} (R) ∥ T (a - a^{'}) ∥_{H^{s}} \leq b^{- 1} B L_{N} (R) ∥ a - a^{'} ∥_{1} \leq b^{- 1} B L_{N} (R) \sqrt{M} ∥ a - a^{'} ∥_{2}$ , using [F5]. Hence $G$ is locally Lipschitz, and [F4] gives a unique maximal solution $x : I \to R^{M}$ of $x^{'} = G (x)$ , $x (0) = T^{- 1} (u_{0})$ , with $I$ an open interval containing $0$ ; $u_{N} : = T \circ x$ is the unique maximal solution of the $X_{N}$ -valued initial value problem $u^{'} = F_{N} (u)$ , $u (0) = u_{0}$ , and every other solution is a restriction of it.

5.1step 3.1step 4.1F4F5

Blow-up alternative. Let $T_{\max} < + \infty$ be the right endpoint of $I$ . If the asserted norm divergence fails, there are $R < \infty$ and times $t_{j} ↑ T_{\max}$ with $∥ u_{N} (t_{j}) ∥_{H^{s}} \leq R$ ; then $x (t_{j}) = T^{- 1} u_{N} (t_{j})$ satisfies $∥ x (t_{j}) ∥_{1} \leq b^{- 1} R$ , so the points $x (t_{j})$ lie in the Euclidean ball of radius $ρ : = b^{- 1} R$ and, by step 4.1, $G$ is bounded by some $M_{0} < + \infty$ and Lipschitz with constant $K : = b^{- 1} B L_{N} (B \sqrt{M} (ρ + 1)) \sqrt{M}$ on the ball of radius $ρ + 1$ . The quantitative Picard-Lindelof theorem [F4] applied to $G$ on that ball therefore gives one fixed $η > 0$ , depending only on $ρ, K, M_{0}$ (hence only on $R, N, ν$ ), such that every initial value problem for $G$ with datum in the ball of radius $ρ$ has a solution on an interval of length $2 η$ ; restarting at $t_{j} > T_{\max} - η$ extends $x$ , hence $u_{N}$ , beyond $T_{\max}$ , contradicting maximality. Hence $∥ u_{N} (t) ∥_{H^{s}} \to + \infty$ as $t ↑ T_{\max}$ ; for any other exponent $s^{'} > 3 / 2$ the norms $∥ \cdot ∥_{H^{s}}$ and $∥ \cdot ∥_{H^{s^{'}}}$ are equivalent on the finite-dimensional space $X_{N}$ by [F5], so $∥ u_{N} (t) ∥_{H^{s^{'}}}$ diverges as well. Conversely, if $∥ u_{N} (t) ∥_{H^{s^{'}}} \leq R$ on $[0, T)$ , $T < + \infty$ , for some $s^{'} > 3 / 2$ , then [F5] transfers the bound to the exponent $s$ and the same restarting argument extends the solution past $T$ .

6.1step 1.1step 2.1step 3.1step 4.1step 5.1step 3.2∎

Claims 1-4 are established by steps 1.1, 2.1, 3.1, 4.1, 5.1 and 3.2; the identity $P_{N} u_{0} \in X_{N}$ for $u_{0} \in H_{σ}^{0}$ holds by definition of $X_{N}$ and [F3].

Remarks

The ordered basis of step 4.1 is a bookkeeping device for the finite-dimensional ODE theory; the estimates use only the two-sided bound of [F5] and, for the blow-up alternative, the equivalence of the norms $∥ \cdot ∥_{H^{s}}$ on the finite-dimensional space $X_{N}$ .
The blow-up alternative is stated for the $H^{s}$ norm with $s > 3 / 2$ because that is the norm in which the restarting argument is quantitative; the local Lipschitz bound is proved in the same norm.

The Galerkin coefficient system: finite-dimensional invariance, local Lipschitz property, and the unique maximal approximation on the torus

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources