Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)
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.

White-noise spectral sequence representation

Statement

Let H be a separable real Hilbert space with a fixed complete orthonormal basis (uj), indexed by J={1,…,m} for m∈N0 or by J=N>0; the empty basis covers H={0}. Let Yx(g)=⟨Kx,g⟩H+ϵZ(g) be the isonormal white-noise experiment with ϵ>0, and write μj=⟨Kx,uj⟩H. For every parameter x and every basis index j, the observations Yx(uj) are independent and have laws N(μj,ϵ2), where N is the scalar normal law defined in the experiment.

For g∈H, set PNg=∑j∈J, j≤N⟨g,uj⟩Huj, with PN=I once all vectors of a finite basis have been included. Then

Yx(g)=L2(P)-lim⁡N→∞∑j∈J, j≤N⟨g,uj⟩HYx(uj).

Thus every finite collection of observation functionals is reconstructed from the coefficient sequence in mean square. This does not assert almost-sure convergence of the full sequence of partial sums, a simultaneous path identity for all test vectors, or an H-valued observation.

More precisely, let CH be the cylinder sigma-algebra on RH, let CJ be the sigma-algebra on RJ generated by its coordinate evaluations, and let Px be the field sampling law. Define S:RH→RJ by S(y)j=y(uj) and Qx=S∗Px, where a pushforward is S∗Px(B)=Px(S−1(B)). There is a measurable map T:(RJ,CJ)→(RH,CH), depending only on the indexed basis, such that for every parameter x,

S∗Px=Qx,T∗Qx=Px,S∘T=id⁡RJ.

These parameter-independent maps give equivalence of the field cylinder experiment and its coefficient experiment. One such map is the following. For k≥1 and g∈H, let Nk(g) be the least integer N≥k with ∥g−PNg∥H≤2−k and put

ag,k(z)=∑j∈J, j≤Nk(g)⟨g,uj⟩Hzj,T(z)(g)={lim⁡k→∞ag,k(z),if the limit exists in R,0,otherwise.

For each fixed x and g, T(S(Yx))(g)=Yx(g) almost surely, and the same holds jointly for each fixed finite list of test vectors. The exceptional event may depend on x and on that list; no intersection over all g∈H is asserted. In dimension zero the coefficient space is a singleton and T returns the field with value zero at g=0.

If H=L2([0,1]) and the basis is one of the wavelet or trigonometric bases used to define the negative Sobolev carrier H(δ), then under countable choice and for δ>1/2 the same coordinate sequence is a Borel Gaussian random element in H(δ) with mean coefficients Kx and noise level ϵ. In infinite dimension it is not an L2([0,1])-valued sample.

Facts & Assumptions

[F1]

Isonormal Gaussian white-noise inverse experiment: The process is linear into L2(P), centered, has covariance E[Z(g)Z(h)]=⟨g,h⟩H, and has independent standard-normal coordinates on every finite orthonormal tuple.

[F2]

Orthonormal families, complete orthonormal systems and Hilbert bases: A complete orthonormal family has dense finite linear span in H; an orthogonal projection onto a finite span is given by the corresponding finite coefficient sum.

[F3]

Cauchy–Schwarz: ∣⟨x,y⟩∣≤∥x∥ ∥y∥, with equality exactly for dependent pairs: For vectors v,w in a real or complex inner-product space, ∣⟨v,w⟩∣≤∥v∥ ∥w∥.

[F4]

Logarithmic negative Sobolev spaces for white noise: For δ>0, H(δ) has squared coefficient norm ∑l,kal−1(log⁡al)−2δ∣clk∣2, and the coefficient map embeds L2([0,1]) continuously into H(δ).

[F5]

White noise is a Borel Gaussian law on the negative Sobolev space: Under countable choice, for the specified wavelet or trigonometric basis and δ>1/2, the independent standard-normal coefficient sequence is almost surely a Borel Gaussian random element of H(δ) and is not an L2([0,1])-valued random element.

[F6]

Chebyshev-Markov inequality for the integral: For any nonnegative measurable f on a measure space and t>0, μ{f≥t}≤t−1∫f dμ; the space need not be finite or discrete.

[F7]

The first Borel-Cantelli lemma for measures: If measurable events have summable probabilities, their limsup has probability zero; independence is not required.

[F8]

Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable: The limsup and liminf of a sequence of measurable real functions are measurable, as is their equality set.

[F9]

Finite measures agreeing on a generating pi-system and on the whole space are equal: Finite measures agreeing on a generating pi-system and on the whole space agree on the generated sigma-algebra.

[F10]

The law of a random element is a probability measure: The pushforward law of a measurable random element is a probability measure.

[A1]

The Axiom of Countable Choice (ACω): Countable choice states that every sequence of nonempty sets has a choice function.

Given: The experiment and hypotheses in the Statement, a fixed complete finite or countable orthonormal basis, and, for the final clause, the stated L2([0,1]) basis and δ>1/2.

Proof

1.1givenF2choosealgebra

For N let VN=span⁡{uj:j∈J, j≤N} and let PNg=∑j∈J, j≤N⟨g,uj⟩Huj. Orthonormality gives g−PNg⊥VN. For any v∈H, expanding the inner product of v=PNv+(v−PNv) gives ∥v∥2=∥PNv∥2+∥v−PNv∥2, so ∥PNv∥≤∥v∥. Given η>0, density of the finite span in [F2] gives w∈VM with ∥g−w∥<η; for N≥M, PNw=w, so ∥g−PNg∥≤∥g−w∥+∥PN(w−g)∥≤2∥g−w∥<2η. Thus PNg→g in norm, with the finite-basis case eventually equal to g.

1.2givenF1algebra

For distinct indices j1,…,jm, [F1] gives independent standard-normal variables Z(uj1),…,Z(ujm). Since ϵ>0, the affine map z↦μjr+ϵz and its inverse are continuous, so Yx(ujr) and its noise coordinate generate the same sigma-algebra; independence therefore transfers. The affine-image definition of N gives each law N(μjr,ϵ2).

1.3givenF1algebra

Put cj=⟨g,uj⟩H. The linearity clause in [F1] applied to the finite sum defining PNg gives Z(PNg)=∑j∈J, j≤NcjZ(uj); linearity of the inner product gives ⟨Kx,PNg⟩H=∑j∈J, j≤Ncjμj. Combining these identities yields Yx(PNg)=∑j∈J, j≤NcjYx(uj).

1.4givenA1F1F4F5

In the carrier case covered by [F4]–[F5], [F1] supplies independent coordinates with the common standard-normal density and [A1] supplies the countable-choice hypothesis of [F5]. Hence [F5] makes the noise coefficient sequence a Borel Gaussian random element of H(δ); [F4] puts each deterministic signal Kx in the same space. Their sum Kx+ϵW is therefore an H(δ)-valued Borel random element, and every continuous linear functional of it is a translate and positive rescaling of the corresponding centered Gaussian functional.

1.5givenF4F5algebra

In the infinite-dimensional function-space case, if Kx+ϵW were an H-valued sample on an event of probability one, then W=((Kx+ϵW)−Kx)/ϵ would also be H-valued there, since Kx∈H and ϵ>0. This contradicts [F5], so the sample is not H-valued.

2.1givenF1F3step 1.1step 1.3algebra

With rN=g−PNg, linearity gives Yx(g)−Yx(PNg)=⟨Kx,rN⟩H+ϵZ(rN). Centering and the covariance identity in [F1] give EZ(rN)=0 and E[Z(rN)2]=∥rN∥H2; expanding the square therefore shows that the squared mean-square error is ∣⟨Kx,rN⟩H∣2+ϵ2∥rN∥H2. By [F3] and step 1.1, both terms tend to zero, proving the asserted mean-square reconstruction. For any finite list of test vectors, the sum of their finitely many squared errors also tends to zero, so the coordinate reconstructions converge jointly in product mean square.

2.2givenF8step 1.1construct

By step 1.1, for each g and k≥1 the set of integers N≥k with ∥g−PNg∥H≤2−k is nonempty. Its least element Nk(g) is uniquely defined, with no choice and no dependence on x, Kx or the observations. For fixed g,k, ag,k is a finite linear combination of coordinate evaluations on RJ, hence is measurable. By [F8], its limsup and liminf are measurable; their equality set, intersected with the set where their common value is finite, is the measurable real-convergence set Ag. Defining T(z)(g) to equal that limit on Ag and zero on its complement is measurable: for a Borel set B⊆R its preimage is Ag∩{lim sup⁡kag,k∈B}, together with Agc if 0∈B. Thus every evaluation of T is measurable, which makes T measurable into CH. Each coordinate of S is a field evaluation, so S is measurable into CJ as well.

3.1givenF3F6F7step 1.3step 2.1step 2.2algebra

Fix x and g. By steps 1.3 and 2.1, the real random variable Dk=ag,k(S(Yx))−Yx(g) satisfies E∣Dk∣2≤(∥Kx∥H2+ϵ2)4−k. For every positive integer r, [F6] applied to ∣Dk∣2 at threshold r−2 gives P{∣Dk∣≥1/r}≤r2(∥Kx∥H2+ϵ2)4−k. The right-hand side is summable in k, so [F7] makes ∣Dk∣<1/r eventually almost surely for each r. The union over r≥1 of these null exceptional events is null: disjointifying the union and using countable additivity bounds its probability by the sum of zeros. Off that union Dk→0, proving T(S(Yx))(g)=Yx(g) almost surely. All limits here concern the explicitly specified representatives at a fixed x,g; the L2 equalities used to compute the error hold almost surely and therefore give exactly the same second moments.

4.1givenF9F10step 2.2step 3.1

The coordinate law Qx=S∗Px and the reconstructed law T∗Qx are probability measures by [F10]; they use only pushforwards of the given process, with no new product-existence assumption. For any finite list g1,…,gn, intersect the finitely many probability-one events in step 3.1. On that intersection the reconstructed and original evaluation vectors agree, so T∗Qx and Px agree on every finite cylinder {y:(y(g1),…,y(gn))∈B} for Borel B⊆Rn. These cylinders form a generating pi-system for CH, and both measures have total mass one, so [F9] gives T∗Qx=Px on CH. This proves equality of laws without any uncountable intersection of probability-one events.

5.1givenF1F2step 1.4step 2.2step 4.1algebra∎

For every basis index j, Nk(uj)≥k≥j once k≥j, so orthonormality gives auj,k(z)=zj then, for every z∈RJ. Consequently T(z)(uj)=zj and S∘T=id⁡RJ everywhere. If J=∅, completeness forces H={0}, every sum defining a0,k is zero, and T returns the zero field; linearity gives Yx(0)=0 almost surely. If J is nonempty and finite, PN=I after its last index, so the same construction reduces to the finite linear reconstruction and all preceding arguments apply. Thus the maps in the Statement establish both sampling-law identities in every allowed dimension. The least-index construction spends no choice principle; the only countable-choice use remains step 1.4.

Coordinate diagram

For a fixed truncation N (with N no larger than the basis length in the finite-dimensional case), define UN(g)=(⟨g,uj⟩H)j=1N, DN(g)=[Yx(PNg)], and SN(a1,…,aN)=[∑j=1NajYx(uj)], where brackets denote equivalence classes in L2(P). The diagram commutes by finite linearity, as proved in step 1.3; the diagonal approximations DN(g) converge to [Yx(g)] in L2(P) by step 2.1. The diagram illustrates these maps and is not used in the proof.

HRNL2(P)L2(P)UNDNSN

Depends on

Used by

Dependency tree · two levels

57 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources