Definition. Coordinate Lebesgue reference measure [fdip-002H]

Let \(\lambda _{\mathbb R}\) be Lebesgue measure restricted to \(\mathcal B(\mathbb R)\), normalized by \(\lambda _{\mathbb R}(\{x\in \mathbb R:a<x\le b\})=b-a\) for \(a<b\). The coordinate Lebesgue measure of a finite real field space is \[\lambda _V=\bigotimes _{v\in V}\lambda _{\mathbb R}\] on \(\mathcal B(X_V)=\Sigma _V\), characterized on Borel rectangles by \[\lambda _V\left (\prod _v A_v\right ) =\prod _v\lambda _{\mathbb R}(A_v).\] Products lie in \([0,\infty ]\), with \(0\cdot \infty =0\); the empty product is \(1\). The reference is fixed by counting coordinates, independently of any quadratic precision.

Existence follows by induction from the sigma-finite product-measure theorem, [tao2011measure, Proposition 1.7.11, pp. 197-199, preliminary version]. Start with \(\lambda _\varnothing =\delta _0\) on \(X_\varnothing =\{0\}\). Each factor is sigma-finite, and the cubes \([-k,k]^V\), \(k\ge 1\), cover with finite masses \((2k)^{|V|}\). Thus the product is sigma-finite. For nonempty \(V\) these masses grow without bound, so \(\lambda _V(X_V)=\infty \); it is not a probability measure. Finite-cube uniqueness handles its infinite total mass.

The real-spin reference convention appears in [friedli2017statistical, Definition 8.1 and Equation (8.3), p. 381, author version revised 22 August 2017]. The model's boundary conditions and density are additional data. No completion or normalizing density is part of \(\lambda _V\).

Mathlib constructs the finite product as MeasureTheory.Measure.pi; its rectangle law MeasureTheory.Measure.pi_pi uses sigma-finite factors. The product-volume convention is MeasureTheory.volume_pi. The empty cases MeasureTheory.Measure.pi_of_empty and MeasureTheory.Measure.pi_empty_univ give Dirac mass and total mass one, respectively.