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.

Lattice ball and shell counts and weight sums on the frequency lattice

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), as the Lebesgue-measure statements quoted below do. Let $w_{k} = (1 + ∣ 2 π k ∣_{2}^{2})^{1 / 2}$ for $k \in Z^{3}$ (Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection).

Ball count. For every $R \geq 0$ , $# {k \in Z^{3} : ∣ k ∣_{2} \leq R} \leq \frac{4 π}{3} (R + \frac{\sqrt{3}}{2})^{3} .$
Shell count. There is an absolute constant $C_{*}$ such that for every integer $m \geq 1$ $# {k \in Z^{3} : m \leq ∣ k ∣_{2} < m + 1} \leq C_{*} (m + 1)^{2};$ the proof exhibits $C_{*} = 240$ .
Weight sums. If $σ > 3 / 2$ then $\sum_{k \in Z^{3}} w_{k}^{- 2 σ} < + \infty$ ; more generally, if $σ - r > 3 / 2$ then $\sum_{k \in Z^{3}} w_{k}^{2 r - 2 σ} < + \infty$ . In particular $\sum_{k \in Z^{3}} (2 π ∣ k ∣_{2})^{2} w_{k}^{- 2 σ} < + \infty$ whenever $σ > 5 / 2$ .
$ℓ^{1}$ bounds. If $σ > 3 / 2$ , then for every family $c : Z^{3} \to C^{3}$ $\sum_{k \in Z^{3}} ∣ c (k) ∣_{2} \leq W_{σ} (\sum_{k \in Z^{3}} w_{k}^{2 σ} ∣ c (k) ∣_{2}^{2})^{1 / 2}, W_{σ} : = (\sum_{k \in Z^{3}} w_{k}^{- 2 σ})^{1 / 2} < + \infty,$ and if $σ > 5 / 2$ , then with $W_{σ}^{'} : = (\sum_{k} (2 π ∣ k ∣_{2})^{2} w_{k}^{- 2 σ})^{1 / 2} < + \infty$ , $\sum_{k \in Z^{3}} 2 π ∣ k ∣_{2} ∣ c (k) ∣_{2} \leq W_{σ}^{'} (\sum_{k \in Z^{3}} w_{k}^{2 σ} ∣ c (k) ∣_{2}^{2})^{1 / 2} .$
Truncation tails. For every integer $N \geq 0$ , every real $r$ and every family $c : Z^{3} \to C^{3}$ , $\sum_{∣ k ∣_{\infty} > N} w_{k}^{2 r} ∣ c (k) ∣_{2}^{2} \leq (2 π (N + 1))^{- 2} \sum_{∣ k ∣_{\infty} > N} w_{k}^{2 r + 2} ∣ c (k) ∣_{2}^{2},$ both sides allowed to be $+ \infty$ ; in particular, for $u \in H^{r + 1}$ the $H^{r}$ -weighted tail beyond $∣ k ∣_{\infty} > N$ is at most $(2 π (N + 1))^{- 2} ∥ u ∥_{H^{r + 1}}^{2}$ .

Facts & Assumptions

Given: The weight family $w_{k} = (1 + 4 π^{2} ∣ k ∣_{2}^{2})^{1 / 2}$ of Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection, with $w_{k} \geq 1$ , $w_{k} \geq 2 π ∣ k ∣_{\infty}$ and $∣ 2 π k_{j} ∣ \leq w_{k}$ for $j = 1, 2, 3$ .

[F1]

A measure is countably additive on pairwise disjoint measurable sets, hence finitely additive: if $A, B$ are disjoint measurable sets then $μ (A \cup B) = μ (A) + μ (B)$ , and monotonicity $A \subseteq B \Rightarrow μ (A) \leq μ (B)$ follows by applying additivity to the disjoint sequence $A, B ∖ A, \emptyset, \emptyset, \dots$ (Measures on sigma-algebras).

[F2]

The half-open box $\prod_{i < 3} (a_{i}, b_{i}]$ is Lebesgue measurable of measure $\prod_{i < 3} (b_{i} - a_{i})$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[F4]

The closed ball of radius $R$ in $R^{3}$ has volume $\frac{4}{3} π R^{3}$ , which is the value $V_{3} (R) = π^{3 / 2} R^{3} / Γ (5 / 2)$ of The volume of a radius- $r$ closed $n$ -ball is $π^{n / 2} r^{n} / Γ (n / 2 + 1)$ .

[F5]

For a family $a : N \to [0, + \infty]$ the nonnegative extended sum is the supremum of the finite partial sums, and the finite sums are the usual ones (Series in the nonnegative extended real line); in particular a nonnegative series converges exactly when its finite partial sums are bounded.

[F6]

For reals $a_{0}, \dots, a_{n - 1}$ and $b_{0}, \dots, b_{n - 1}$ , $∣ \sum_{k < n} a_{k} b_{k} ∣ \leq (\sum_{k < n} a_{k}^{2})^{1 / 2} (\sum_{k < n} b_{k}^{2})^{1 / 2}$ (The Cauchy-Schwarz inequality for finite sums).

[F7]

If $f : [0, \infty) \to R$ is nonincreasing and nonnegative, then $\sum_{k \geq 0} f (k)$ converges if and only if the integrals $\int_{0}^{N} f$ are bounded (The integral test: for $f \geq 0$ nonincreasing on $[0, \infty)$ , $\sum_{k} f (k)$ converges if and only if the sequence $(\int_{0}^{N} f)_{N}$ is bounded, with $\int_{0}^{N} f \leq \sum_{k < N} f (k) \leq f (0) + \int_{0}^{N} f$ ); this yields the convergence of $\sum_{m \geq 1} m^{- p}$ for $p > 1$ .

Proof

technique · direct; count lattice points by packing unit boxes into a ball, then compare the weight sums with convergent $p$-series and apply Cauchy-Schwarz to finite partial sums

Given: The weight family $w_{k}$ and the facts [F1]-[F7].

1.1givenF2

For $k \in Z^{3}$ let $H_{k} : = \prod_{i = 1}^{3} (k_{i} - \frac{1}{2}, k_{i} + \frac{1}{2}]$ be the half-open unit box centred at $k$ . Distinct $H_{k}$ are pairwise disjoint: if $k \neq l$ then $∣ k_{i} - l_{i} ∣ \geq 1$ for some $i$ , and the half-open intervals $(k_{i} - \frac{1}{2}, k_{i} + \frac{1}{2}]$ and $(l_{i} - \frac{1}{2}, l_{i} + \frac{1}{2}]$ are disjoint. Each $H_{k}$ is measurable of measure $1$ by [F2], and $H_{k} \subseteq \overline{B} (0, R + \frac{\sqrt{3}}{2})$ whenever $∣ k ∣_{2} \leq R$ , because for $x \in H_{k}$ one has $∣ x ∣_{2} \leq ∣ k ∣_{2} + ∣ x - k ∣_{2} \leq R + \sqrt{3} / 2$ .

2.1step 1.1F1F4

Let $N (R) : = # {k \in Z^{3} : ∣ k ∣_{2} \leq R}$ . The union $U_{R} : = ⋃_{∣ k ∣_{2} \leq R} H_{k}$ is a finite disjoint union of measurable sets, so by induction on the number of boxes and [F1] one has $λ_{3} (U_{R}) = \sum_{∣ k ∣_{2} \leq R} λ_{3} (H_{k}) = N (R)$ . Since $U_{R} \subseteq \overline{B} (0, R + \sqrt{3} / 2)$ by step 1.1 and the closed ball is measurable, monotonicity in [F1] gives $N (R) = λ_{3} (U_{R}) \leq λ_{3} (\overline{B} (0, R + \sqrt{3} / 2)) = \frac{4}{3} π (R + \sqrt{3} / 2)^{3}$ by [F4]; this is claim 1.

2.2step 1.1F1F4algebra

Put $c : = \sqrt{3} / 2 < 1$ . The disjoint unit boxes $H_{k}$ for $m \leq ∣ k ∣_{2} < m + 1$ lie in the annulus $m - c \leq ∣ x ∣_{2} < m + 1 + c$ , since $∣ x - k ∣_{2} \leq c$ . For every $0 < ϵ < m - c$ , their union is contained in the closed outer ball of radius $m + 1 + c$ minus the closed inner ball of radius $m - c - ϵ$ . Its measure is at most $\frac{4}{3} π [(m + 1 + c)^{3} - (m - c - ϵ)^{3}]$ by [F1] and [F4]; letting $ϵ ↓ 0$ bounds the union by $\frac{4}{3} π [(m + 1 + c)^{3} - (m - c)^{3}]$ , without needing a separate sphere-measure assertion. By finite additivity each box has volume one, so the shell count is bounded by this volume. Since $m \geq 1$ and $c < 1$ , the difference of cubes is at most $(m + 2)^{3} - (m - 1)^{3} = 9 m^{2} + 9 m + 9 \leq 27 (m + 1)^{2}$ . Thus the shell count is at most $36 π (m + 1)^{2} \leq 240 (m + 1)^{2}$ , preserving the stated $C_{*} = 240$ .

3.1step 2.2F4F5F7given

Write $Σ_{σ} : = \sum_{k \in Z^{3}} w_{k}^{- 2 σ}$ as a nonnegative extended sum and split it into the mode $k = 0$ and the shells of index $m \geq 1$ . Using claim 2, $w_{k}^{2} \geq 4 π^{2} m^{2}$ on the $m$ -th shell and $1 \leq m$ , we get the finite-partial-sum bound $\sum_{∣ k ∣_{2} \leq M} w_{k}^{- 2 σ} \leq 1 + 240 (4 π^{2})^{- σ} \sum_{1 \leq m \leq M} (m + 1)^{2} m^{- 2 σ}$ for $M \geq 1$ ; since $(m + 1)^{2} \leq 4 m^{2}$ there is a constant $C$ with $\sum_{∣ k ∣_{2} \leq M} w_{k}^{- 2 σ} \leq 1 + C \sum_{m \leq M} m^{2 - 2 σ}$ for every $M$ . If $σ > 3 / 2$ then $2 σ - 2 > 1$ , so $\sum_{m \geq 1} m^{2 - 2 σ}$ converges by [F7]; by [F5] the finite partial sums of $Σ_{σ}$ are bounded, so $Σ_{σ} < + \infty$ . Replacing $σ$ by $σ - r$ gives the general weight sum $\sum_{k} w_{k}^{2 r - 2 σ} = \sum_{k} w_{k}^{- 2 (σ - r)} < + \infty$ whenever $σ - r > 3 / 2$ , and with $r = 1$ and $σ > 5 / 2$ this gives $\sum_{k} (2 π ∣ k ∣_{2})^{2} w_{k}^{- 2 σ} \leq \sum_{k} w_{k}^{2 - 2 σ} < + \infty$ , since $2 π ∣ k ∣_{2} \leq w_{k}$ ; this is claim 3.

4.1step 3.1F5F6

For claim 4 fix a family $c$ and a finite $F \subseteq Z^{3}$ . Cauchy-Schwarz [F6] applied to the lists $a_{k} = w_{k}^{- σ}$ and $b_{k} = w_{k}^{σ} ∣ c (k) ∣_{2}$ , $k \in F$ , gives $\sum_{k \in F} ∣ c (k) ∣_{2} \leq (\sum_{k \in F} w_{k}^{- 2 σ})^{1 / 2} (\sum_{k \in F} w_{k}^{2 σ} ∣ c (k) ∣_{2}^{2})^{1 / 2} \leq W_{σ} ∥ c ∥_{ℓ_{σ}^{2}}$ , with $W_{σ}$ finite by claim 3; taking the supremum over finite $F$ by [F5] gives the first bound. The second bound is the same computation with the lists $a_{k} = 2 π ∣ k ∣_{2} w_{k}^{- σ}$ and $b_{k} = w_{k}^{σ} ∣ c (k) ∣_{2}$ , whose first factor is $W_{σ}^{'} < \infty$ by claim 3 with $r = 1$ and $σ > 5 / 2$ .

5.1givenF5algebra∎

For claim 5 let $∣ k ∣_{\infty} > N$ , so $2 π ∣ k ∣_{\infty} \geq 2 π (N + 1)$ and hence $w_{k} \geq 2 π (N + 1)$ by the given inequality $w_{k} \geq 2 π ∣ k ∣_{\infty}$ ; therefore $w_{k}^{2 r} \leq (2 π (N + 1))^{- 2} w_{k}^{2 r + 2}$ for every such $k$ . Summing this pointwise inequality over the finite sets ${∣ k ∣_{\infty} > N, ∣ k ∣_{2} \leq M}$ and taking the supremum in $M$ by [F5] gives claim 5; for $u \in H^{r + 1}$ the right-hand side is at most $(2 π (N + 1))^{- 2} ∥ u ∥_{H^{r + 1}}^{2}$ .

Remarks

The count in claim 1 is the standard packing of unit half-open cubes into the ball of radius $R + \sqrt{3} / 2$ ; it is sharp up to the constant, which is all the later estimates use.
Claim 3 and claim 4 are the only place where the threshold $σ > 3 / 2$ for the torus dimension $3$ enters: the lattice sum $\sum_{k} w_{k}^{- 2 σ}$ converges exactly when $2 σ > 3$ , and the $ℓ^{1}$ bound for coefficients is what forces Sobolev fields of order $> 3 / 2$ to have absolutely convergent Fourier series, and hence continuous representatives.
The tail inequality in claim 5 is the quantitative form of the strong convergence of the Fourier truncations: it shows that the truncation error in $H^{r}$ is bounded by the $(r + 1)$ -norm divided by the first omitted frequency.

Lattice ball and shell counts and weight sums on the frequency lattice

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources