Center-Fiber Moment Representation

Abstract

Even difference moments are Fourier transforms of nonnegative center-fiber densities.

Theorem 1.1 (The center-fiber density represents the even moment).

$$\begin{array}{c}\forall \phi :\mathbb{R}\to \mathbb{R},m\in \mathbb{N},t\in \mathbb{R},\\ \mathrm{Continuous}\left(\phi \right)\wedge (\forall x\in \mathbb{R},0\le \phi \left(x\right))\wedge \\ \mathrm{Integrable}\left(((u,v)\mapsto v^{2m}\phi \left(\frac{u+v}{2}\right)\phi \left(\frac{u-v}{2}\right))\right)\Rightarrow \\ \left(C_m\right)\left(u\right)=\frac{1}{2\mathrm{factorial}\left(2m\right)}{\int }_{\mathbb{R}}{v}^{2m}\phi \left(\frac{u+v}{2}\right)\phi \left(\frac{u-v}{2}\right)dv,\\ \left({\mathcal{J}}_m\right)\left(t\right)=\frac{1}{\mathrm{factorial}\left(2m\right)}{\int }_{\mathbb{R}}{\int }_{\mathbb{R}}\phi \left(x\right)\phi \left(y\right){x-y}^{2m}\exp \left(itx+y\right)dydx,\\ \left({\mathcal{J}}_m\right)\left(t\right)={\int }_{\mathbb{R}}\left(C_m\right)\left(u\right)\exp \left(itu\right)du\wedge \forall u\in \mathbb{R},0\le \left(C_m\right)\left(u\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Fourier/CenterFiberMomentRepresentation.center_fiber_moment_representation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let phi be a continuous nonnegative real function. The source did not state the positivity assumption needed for the claimed pointwise nonnegativity of C_m, so it is explicit here.

We also require absolute integrability of the real center-fiber moment kernel. This supplies the missing analytic hypothesis for Fubini and for both displayed Lebesgue integrals.

The proof applies the real linear map (x,y) maps to (x+y,x-y). Its determinant is minus two, so the inverse Jacobian contributes the factor one half in C_m.

Pinned Mathlib supplies Haar-measure transport for an invertible linear map and Fubini’s theorem. Evenness of the exponent and nonnegativity of phi give C_m(u) nonnegative for every real u.

References

• Truth anchor: D5/S3/Fourier/CenterFiberMomentRepresentation.center_fiber_moment_representation