Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-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.

Periodic vector Sobolev spaces on the three-torus, the weight family, and the Leray projection

Definition

Assume the Axiom of Countable Choice ACω (The Axiom of Countable Choice (ACω)), which is used by the imported Fourier-basis theorem quoted below.

The three-torus and its measure. Let T:=R/Z be the one-dimensional torus with its quotient topology and its normalized Haar integral mT (The one-dimensional torus and its normalized Haar integral); T is compact Hausdorff (Finite tori are compact Hausdorff spaces separated by characters). Put T3:=T×T×T with the finite product topology. Let dx:=mT⊗mT⊗mT be the product measure on the Borel σ-algebra of T3 (The product measure of two sigma-finite measure spaces, Lebesgue measurable sets, the family L(Rn), and the restricted set function λn); being a product of probability measures it is a probability measure. For a vector k=(k1,k2,k3)∈Z3 and x=(x1,x2,x3)∈T3 define the character ek(x):=exp⁡(2πi (k1x1+k2x2+k3x3))=e2πi k⋅x, where each xj is inserted through any real representative and exp⁡ is the complex exponential (Fourier coefficients and trigonometric polynomials on the torus); the definition does not depend on the representatives. Then ∣ek(x)∣=1, ekel=ek+l, and e−k=ek‾.

Function spaces. Write L2:=L2(T3;R3) for the real Hilbert space of (equivalence classes of) real Borel vector fields u:T3→R3 with ∫T3∣u∣22 dx<+∞, inner product ⟨u,v⟩:=∫T3u⋅v dx and norm ∣u∣2:=⟨u,u⟩1/2; here u⋅v is the Euclidean inner product of R3 (Complex Lp classes and Euclidean test-function conventions). Similarly L1(T3;C3) denotes the integrable complex vector fields.

Fourier coefficients. For u∈L1(T3;C3) and k∈Z3 define u^(k):=∫T3u(x) e−k(x) dx ∈C3. The integral depends only on the class of u. A field u∈L1 is real almost everywhere if and only if u^(−k)=u^(k)‾ for every k∈Z3; the forward direction uses u‾^(k)=u^(−k)‾, and the reverse uses L1 Fourier uniqueness, proved below. On the circle this uniqueness follows from Fejer means converge in L^p for 1 <= p < infinity with p=1: zero coefficients give zero Fejer means, whose L1 limit is the function. To pass to Td for d=2,3, use Fubini's theorem for L^1 functions on a sigma-finite product: for fixed k′∈Zd−1, gk′(x1)=∫Td−1u(x1,x′)e−k′(x′)dx′ is in L1(T) and all its coefficients vanish. Hence gk′=0 almost everywhere. The countable union of the exceptional sets over k′ is null. For every remaining x1, the L1 section in x′ has all coefficients zero, so induction in d makes it zero almost everywhere. Fubini then makes u=0 almost everywhere on Td. Apply this uniqueness to u−u‾ to obtain the reverse real-valuedness implication. For u∈L2⊂L1 (finite measure) the coefficient map is the one of the imported theorem, which states: (ek)k∈Z3 is an orthonormal basis of the complex Hilbert space L2(T3;C), the finite-subset-net expansion u=∑ku^(k)ek and the Parseval identities hold, and u↦u^ is a surjective linear isometry of L2(T3;C) onto ℓ2(Z3;C) (The Fourier basis and Parseval's identity on the finite torus); the last statement applied componentwise gives ⟨u,v⟩=∑ku^(k)⋅v^(k)‾ for real u,v∈L2.

Weights. For k∈Z3 set wk:=(1+∣2πk∣22)1/2=(1+4π2∣k∣22)1/2 ≥1, so that wk≥∣2πkj∣ for j=1,2,3 and wk+l≤wk+wl for all k,l∈Z3.

The coefficient space and Hs. For s∈R let ℓs2 be the complex Hilbert space of all c:Z3→C3 with ∥c∥ℓs22:=∑k∈Z3wk2s∣c(k)∣22<+∞,⟨c,d⟩ℓs2:=∑k∈Z3wk2s c(k)⋅d(k)‾, and let ℓs,R2:={c∈ℓs2:c(−k)=c(k)‾ ∀k}. The set ℓs,R2 is closed in ℓs2 and is a real-linear subspace; on it the Hermitian pairing ⟨⋅,⋅⟩ℓs2 is real valued, because the substitution k↦−k 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 L2 onto ℓ0,R2. For s≥0 define Hs(T3;R3):={u∈L2:u^∈ℓs,R2},∥u∥Hs:=∥u^∥ℓs2. For s<0 define Hs to be the completion of the real trigonometric polynomials in the same weighted coefficient norm, equivalently the space of formal real coefficient families ℓs,R2. For an element of this completion u^(k) means its coefficient, not an integral of an assumed L2 function. The embedding of L2 into these negative-order spaces is its coefficient map. Truncation makes finite families dense, so this completion is all of ℓs,R2, not merely the coefficient families of L2 fields. Consequently each Hs is a real Hilbert space isometric to ℓs,R2 through u↦u^, and ∥u∥H0=∣u∣2. If s≥t then Hs⊆Ht and ∥u∥Ht≤∥u∥Hs. The trigonometric polynomials are the fields p=∑k∈Fckek with F⊆Z3 finite and c−k=ck‾ (equivalently, real coefficient families of finite support); they belong to every Hs, and the finitely supported families are dense in each ℓs,R2 (truncate a family to ∣k∣∞≤M and let M→∞), so trigonometric polynomials are dense in every Hs.

Scalar spaces. For s∈R define ℓs2(Z3;C) to consist of families c:Z3→C with ∑kwk2s∣c(k)∣2<∞, with pairing ∑kwk2sc(k)d(k)‾; its real subspace is specified by c(−k)=c(k)‾. For s≥0, Hs(T3;R) consists of real scalar L2 classes with this weighted coefficient norm; for s<0 it is the completion of real scalar trigonometric polynomials, identified with the real coefficient subspace. Scalar Fourier coefficients are f^(k)=∫fe−k dx when f∈L1, and otherwise denote the completion coordinates. Parseval and truncation give the scalar Hilbert-space and density assertions exactly as above. A vector belongs to Hs(T3;R3) exactly when each of its three scalar components belongs to Hs(T3;R), with ∥u∥Hs2=∑j=13∥uj∥Hs2. Below the value type distinguishes scalar and vector Hs; Λs, ∂j and Δ have the same multipliers for scalars, ∇ maps scalar to vector spaces, and div⁡ maps vector to scalar spaces.

The operators Λs, ∂j, Δ, ∇ and div⁡. For s,t∈R and u∈Ht define Λsu∈Ht−s by the coefficient rule Λsu^(k):=wks u^(k); then Λs is a linear isometric isomorphism of Ht onto Ht−s, Λ0=id, ΛsΛt=Λs+t, and Λ−s is the inverse of Λs. For j=1,2,3 and u∈Hs+1 define ∂ju∈Hs by ∂ju^(k):=2πi kj u^(k); for u∈Hs+2 define Δu∈Hs by Δu^(k):=−4π2∣k∣22 u^(k); for a scalar field f with coefficients f^(k)∈C in the scalar spaces just defined, define ∇f∈Hs for f∈Hs+1 by ∇f^(k):=2πi k f^(k); and for u∈Hs+1 define div⁡u:=∑j=13∂juj∈Hs. These operators satisfy ∥∂ju∥Hs≤∥u∥Hs+1, ∥Δu∥Hs≤∥u∥Hs+2, and for every integer m≥1, Λ2m=(I−Δ)m, the identity following coefficientwise from wk2=1+4π2∣k∣22. On trigonometric polynomials all four operators agree with the classical coordinatewise derivatives and divergence computed from the smooth functions x↦e2πik⋅x, by the classical rules ∂jek=2πikjek; this is the convention in which the notation is used below.

Divergence-free fields and the Leray projection. For s∈R put Hσs(T3;R3):={ u∈Hs:k⋅u^(k)=0 for every k∈Z3 }; this is a closed real-linear subspace of Hs, and div⁡u=0 in Hs for u∈Hσs+1. For k≠0 let πk∈L(C3) be the orthogonal projection onto the hyperplane {k}⊥, πkv:=v−k⋅v∣k∣22 k, and set π0:=idC3. Define the Leray projection P by Pu^(k):=πku^(k)(k∈Z3). Then: P maps Hs linearly into Hσs, and ∥Pu∥Hs≤∥u∥Hs; P2=P; P is self-adjoint on Hs, i.e. ⟨Pu,v⟩Hs=⟨u,Pv⟩Hs for all u,v∈Hs; P commutes with each Λt, with each ∂j, and with Δ wherever these are defined; and the identity div⁡(Pu)=0 holds in Hs−1 for u∈Hs. Moreover every u∈Hs has the orthogonal decomposition u=Pu+∇f,f∈Hs+1,f^(0)=0,⟨Pu,∇f⟩Hs=0. Here zero mean means zero coefficient at 0 (the usual integral when the field is integrable); orthogonality for all real orders is in the Hs pairing. The scalar element f is determined by f^(0):=0 and f^(k):=k⋅u^(k)2πi ∣k∣22 for k≠0; here f∈Hs+1 because wk2(s+1)∣f^(k)∣2≤C wk2s∣u^(k)∣2 for k≠0, and ∇f^(k)=(k⋅u^(k)/∣k∣22)k=u^(k)−πku^(k). In particular P∇f=0 for every f with ∇f∈Hs, so P is the orthogonal projection of Hs onto Hσs. On smooth fields the decomposition u=Pu+∇f derived above from the Fourier coefficients is called the Hodge decomposition of the torus; the operator P is the Leray projection of the fluid literature.

Time-dependent fields. For an interval [0,T] with T>0 and s∈R, let C([0,T],Hs) denote the set of continuous maps from [0,T] to the metric space (Hs,∥⋅∥Hs), with ∥u∥C([0,T],Hs):=sup⁡0≤t≤T∥u(t)∥Hs. For a map u:[0,T]×T3→R3 of class C∞ we mean that every mixed partial derivative ∂tr∂xαu exists and is continuous on [0,T]×T3, with one-sided time derivatives at t=0,T.

Remarks

  • The whole definition is built on the imported torus Fourier theory, so the countable-choice assumption and the identification of L2 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 ∂j is 2πikj with ∣2πkj∣≤wk, while wk itself is the symbol of Λ1 and wk2 is the symbol of I−Δ.
  • The definition of Hs 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

Dependency tree · 2 levels

Sources