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.
Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection
Definition
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()), which is used by the imported Fourier-basis theorem quoted below.
The three-torus and its measure. Let be the one-dimensional torus with its quotient topology and its normalized Haar integral (The one-dimensional torus and its normalized Haar integral); is compact Hausdorff (Finite tori are compact Hausdorff spaces separated by characters). Put with the finite product topology. Let be the product measure on the Borel -algebra of (The product measure of two sigma-finite measure spaces, Lebesgue measurable sets, the family , and the restricted set function ); being a product of probability measures it is a probability measure. For a vector and define the character where each is inserted through any real representative and is the complex exponential (Fourier coefficients and trigonometric polynomials on the torus); the definition does not depend on the representatives. Then , , and .
Function spaces. Write for the real Hilbert space of (equivalence classes of) real Borel vector fields with , inner product and norm ; here is the Euclidean inner product of (Complex Lp classes and Euclidean test-function conventions). Similarly denotes the integrable complex vector fields.
Fourier coefficients. For and define The integral depends only on the class of . A field is real almost everywhere if and only if for every ; the forward direction uses , and the reverse uses Fourier uniqueness, proved below. On the circle this uniqueness follows from Fejer means converge in L^p for 1 <= p < infinity with : zero coefficients give zero Fejer means, whose limit is the function. To pass to for , use Fubini's theorem for L^1 functions on a sigma-finite product: for fixed , is in and all its coefficients vanish. Hence almost everywhere. The countable union of the exceptional sets over is null. For every remaining , the section in has all coefficients zero, so induction in makes it zero almost everywhere. Fubini then makes almost everywhere on . Apply this uniqueness to to obtain the reverse real-valuedness implication. For (finite measure) the coefficient map is the one of the imported theorem, which states: is an orthonormal basis of the complex Hilbert space , the finite-subset-net expansion and the Parseval identities hold, and is a surjective linear isometry of onto (The Fourier basis and Parseval's identity on the finite torus); the last statement applied componentwise gives for real .
Weights. For set so that for and for all .
The coefficient space and . For let be the complex Hilbert space of all with and let . The set is closed in and is a real-linear subspace; on it the Hermitian pairing is real valued, because the substitution shows that it equals its own conjugate. By the imported theorem the coefficient map restricts to a bijection of the set of real classes of onto . For define For define to be the completion of the real trigonometric polynomials in the same weighted coefficient norm, equivalently the space of formal real coefficient families . For an element of this completion means its coefficient, not an integral of an assumed function. The embedding of into these negative-order spaces is its coefficient map. Truncation makes finite families dense, so this completion is all of , not merely the coefficient families of fields. Consequently each is a real Hilbert space isometric to through , and . If then and . The trigonometric polynomials are the fields with finite and (equivalently, real coefficient families of finite support); they belong to every , and the finitely supported families are dense in each (truncate a family to and let ), so trigonometric polynomials are dense in every .
Scalar spaces. For define to consist of families with , with pairing ; its real subspace is specified by . For , consists of real scalar classes with this weighted coefficient norm; for it is the completion of real scalar trigonometric polynomials, identified with the real coefficient subspace. Scalar Fourier coefficients are when , and otherwise denote the completion coordinates. Parseval and truncation give the scalar Hilbert-space and density assertions exactly as above. A vector belongs to exactly when each of its three scalar components belongs to , with . Below the value type distinguishes scalar and vector ; , and have the same multipliers for scalars, maps scalar to vector spaces, and maps vector to scalar spaces.
The operators , , , and . For and define by the coefficient rule then is a linear isometric isomorphism of onto , , , and is the inverse of . For and define by for define by ; for a scalar field with coefficients in the scalar spaces just defined, define for by ; and for define . These operators satisfy , , and for every integer , , the identity following coefficientwise from . On trigonometric polynomials all four operators agree with the classical coordinatewise derivatives and divergence computed from the smooth functions , by the classical rules ; this is the convention in which the notation is used below.
Divergence-free fields and the Leray projection. For put this is a closed real-linear subspace of , and in for . For let be the orthogonal projection onto the hyperplane , and set . Define the Leray projection by Then: maps linearly into , and ; ; is self-adjoint on , i.e. for all ; commutes with each , with each , and with wherever these are defined; and the identity holds in for . Moreover every has the orthogonal decomposition Here zero mean means zero coefficient at (the usual integral when the field is integrable); orthogonality for all real orders is in the pairing. The scalar element is determined by and for ; here because for , and . In particular for every with , so is the orthogonal projection of onto . On smooth fields the decomposition derived above from the Fourier coefficients is called the Hodge decomposition of the torus; the operator is the Leray projection of the fluid literature.
Time-dependent fields. For an interval with and , let denote the set of continuous maps from to the metric space , with . For a map of class we mean that every mixed partial derivative exists and is continuous on , with one-sided time derivatives at .
Remarks
- The whole definition is built on the imported torus Fourier theory, so the countable-choice assumption and the identification of classes with weighted coefficient families are inherited from The Fourier basis and Parseval's identity on the finite torus; no other choice principle is used.
- The weights are normalized so that differentiation costs one weight: the symbol of is with , while itself is the symbol of and is the symbol of .
- The definition of is the Fourier-coefficient definition used in the fluid literature on the torus; the equivalent description by weak derivatives is not used anywhere below, so no extension theory is presupposed.
Depends on
The one-dimensional torus and its normalized Haar integral
Fourier coefficients and trigonometric polynomials on the torus
The Fourier basis and Parseval's identity on the finite torus
The Axiom of Countable Choice ()
Complex Lp classes and Euclidean test-function conventions
Lebesgue measurable sets, the family , and the restricted set function
The product measure of two sigma-finite measure spaces
Finite tori are compact Hausdorff spaces separated by characters
Fejer means converge in L^p for 1 <= p < infinity
Fubini's theorem for L^1 functions on a sigma-finite product
Dependency tree · 2 levels
Sources
- E. Wiedemann (ed. J. Skipper), Lecture Notes: Navier-Stokes Equations (Universität Ulm, WS 2018/19), Section 2.1 (Fourier characterisation of Sobolev spaces on the torus T^3, Definitions 2.1-2.2) and Section 2.2 (divergence-free fields H, the Helmholtz decomposition Theorem 2.6, the Leray projection Definition 2.7 and the commutation Lemma 2.8)
- A. J. Majda and A. L. Bertozzi, Vorticity and Incompressible Flow (Cambridge Texts in Applied Mathematics, CUP 2002), Subsection 1.9.1 (Fourier series convention (1.99)-(1.102) on one-periodic fields) and Proposition 1.18 with formula (1.98) (Hodge decomposition on the torus and the multiplier k⊗k/|k|^2)