Continuous Integral Versions of L2 Primitives
Abstract
A continuous L2 derivative yields a measurable primitive with continuous paths on its original finite measure space.
Theorem 1.1 (A common set of continuous paths).
Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/L2ContinuousPrimitive.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let Omega be any measurable space and P a finite measure. Let f and u map the whole real line to real L2(P), with u continuous. Let g(t,z) be jointly measurable and, for every fixed t, equal P-almost everywhere to the chosen representative u(t)(z). Assume, for every real t, f(t)=f(0)+the Bochner integral of u from 0 to t.
Define X(t,z)=f(0)(z)+the oriented integral of g(s,z) from 0 to t. Then X is jointly measurable, its paths on the whole real line are continuous on one common P-almost-everywhere set, and at every fixed t it equals f(t)(z) P-almost everywhere. Equality to arbitrary chosen representatives is only asserted at each fixed time, not simultaneously at all times.
Continuity of u and finiteness of P imply integrability of g on every compact time interval times Omega. Testing against indicator functions in L2 and using Fubini identifies the representative of each Bochner integral. A countable exhaustion by bounded intervals gives one set of locally integrable sample functions, hence continuous primitives. Neither compact product integrability nor separate Bochner integrability is an additional hypothesis.
References
- Truth anchor:
D5/S3/Fourier/Asymptotics/L2ContinuousPrimitive.result