Reference measure for real fields [fdip-003U]
✍️sourceAGENTDRAFTED
- October 30, 2026
Reference measure for real fields [fdip-003U]
✍️sourceAGENTDRAFTED
- October 30, 2026
The 4 real field values on the four-cycle range over an infinite configuration space. Before weighting configurations by an action, a reference volume must specify how they are counted. The counting-coordinate measure assigns volume one to the box in which each field value lies between zero and one, independently of the edge weights and mass. It gives infinite volume to the whole space.
The real field topology and its Borel sets make coordinate maps measurable. Reindexing and splitting preserve product volume, while linear changes require a Jacobian. A subspace's induced volume supplies its own reference measure. These conventions determine the integrals defining positive Gaussian laws and constrained massless laws.
Definition 1. The topology of real fields [fdip-002C]AGENTDRAFTED
- October 25, 2026
Definition 1. The topology of real fields [fdip-002C]AGENTDRAFTED
- October 25, 2026
For a finite set \(V\), put \(X_V=\operatorname {Map}(V,\mathbb R)\), the real vertex-field space. Its indicator fields \(\delta _v\) form the finite function basis, so \(x=\sum _{v\in V}x(v)\delta _v\). Use the counting inner product \(h_V(x,y)=\sum _vx(v)y(v)\) and its perfect duality. The carrier \(V\) is finite; the set \(X_V\) of configurations is generally infinite. For \(V=\varnothing \), \(X_V=\{0\}\).
The real field topology is the finite product of the usual topology on \(\mathbb R\). Its basic open sets are boxes \(\prod _{v\in V}O_v\) with every \(O_v\) open.
For a topological space \(Y\), a map \(f:Y\to X_V\) is continuous if and only if every coordinate \(y\mapsto f(y)(v)\) is continuous. Consequently every real linear map between finite field spaces is continuous, and every linear isomorphism is a homeomorphism.
Proof.
- October 25, 2026
Proof.
- October 25, 2026
Evaluation \(x\mapsto x(v)\) is continuous by the product topology. Conversely, the inverse image of a basic box is the finite intersection \(\bigcap _v\{y:f(y)(v)\in O_v\}\), which is open if all coordinates are continuous. For a linear map \(T:X_V\to X_W\), the identity \((Tx)(w)=\sum _vx(v)(T\delta _v)(w)\) makes each output coordinate a finite linear combination of continuous inputs. Apply this also to the inverse when \(T\) is invertible. The empty product has the single basic box \(X_\varnothing \); the same statements hold directly.
Pointwise addition, scalar multiplication and \(h_V\) are continuous by finite sums and products of coordinates. The counting form is positive: if \(x\ne 0\), some \(x(v)^2>0\). Its perfectness can also be read directly: for a linear functional \(\ell \), put \(a(v)=\ell (\delta _v)\); then \(\ell (x)=h_V(a,x)\), uniquely by evaluation on the indicators. These are the real specializations of the cited field and duality constructions.
Definition 2. Borel sets of real fields [fdip-002D]AGENTDRAFTED
- October 25, 2026
Definition 2. Borel sets of real fields [fdip-002D]AGENTDRAFTED
- October 25, 2026
A sigma-algebra on a set \(X\) is a family of subsets containing \(X\) and closed under complements and countable unions. It is also closed under countable intersections, by taking complements. The Borel sigma-algebra \(\mathcal B(X)\) of a topological space is the smallest sigma-algebra containing all its open sets; see [tao2011measure, Definition 1.4.16, p. 87, preliminary version].
On the real field space, define the coordinate-product sigma-algebra \(\Sigma _V\) to be generated by all cylinders \(\{x:x(v)\in B\}\), where \(v\in V\) and \(B\in \mathcal B(\mathbb R)\). This is the product construction of [tao2011measure, Section 1.7.4, pp. 194-195, preliminary version]. The Borel-product proposition identifies it with \(\mathcal B(X_V)\). We use this Borel structure without completion: no additional subsets of null sets are adjoined.
For the singleton \(X_\varnothing \), the Borel structure is \(\{\varnothing ,X_\varnothing \}\). A product of completed factor sigma-algebras need not be the completed product sigma-algebra; these constructions are distinguished in [tao2011measure, p. 94 and Exercise 1.7.19, p. 195, preliminary version].
Proposition 3. Borel sets and finite coordinate products [fdip-002E]AGENTDRAFTED
- October 25, 2026
Proposition 3. Borel sets and finite coordinate products [fdip-002E]AGENTDRAFTED
- October 25, 2026
For every finite real field space, \[\mathcal B(X_V)=\Sigma _V.\] Here \(\Sigma _V\) is the coordinate-product sigma-algebra. This finite-coordinate assertion, including dimension zero, follows by the direct argument below; compare [tao2011measure, Exercises 1.7.18-1.7.19, pp. 194-195, preliminary version].
Proof.
- October 25, 2026
Proof.
- October 25, 2026
Every evaluation is continuous by Definition 1. For fixed \(v\), the subsets of \(\mathbb R\) whose evaluation preimages are Borel form a sigma-algebra containing all open sets, hence all Borel sets. Thus each cylinder is Borel and \(\Sigma _V\subseteq \mathcal B(X_V)\).
Rational open intervals form a countable basis of \(\mathbb R\). Their finite coordinate products form a countable basis of \(X_V\). Each is a finite intersection of cylinder sets and belongs to \(\Sigma _V\). An arbitrary open set is the union of the basis elements it contains; this is a countable union, proving the reverse inclusion. For empty \(V\), the one basic box is the singleton itself, and both sigma-algebras are \(\{\varnothing ,X_V\}\).
Mathlib's Pi.borelSpace requires countable indices,
second-countable topological factors and their Borel measurable structures.
Finite real products meet these assumptions. The less restrictive
pi_le_borel_pi gives only one inclusion, not the displayed equality.
Definition 4. Measurable observables and maps [fdip-002F]AGENTDRAFTED
- October 25, 2026
Definition 4. Measurable observables and maps [fdip-002F]AGENTDRAFTED
- October 25, 2026
A measurable map \(f:(X,\Sigma )\to (Y,\mathcal T)\) satisfies \(f^{-1}(B)\in \Sigma \) for every \(B\in \mathcal T\). A Borel observable on \(X_V\) is a measurable real-valued function for \(\mathcal B(X_V)\) and \(\mathcal B(\mathbb R)\). This is the preimage convention of [tao2011measure, Definition 1.4.32 and Remark 1.4.33, pp. 95-96, preliminary version].
Compositions of measurable maps are measurable because \((g\circ f)^{-1}(B)=f^{-1}(g^{-1}(B))\). The coordinate criterion supplies the maps used for real fields. Measurability does not imply integrability. The integrable-observable space is a vector space, whereas polynomial functions form a separate observable algebra; finite \(V\) does not make the configuration set \(X_V\) finite.
Remark 5. Topology, Borel sets and coordinate observables [fdip-004C]AGENTDRAFTED
- October 31, 2026
Remark 5. Topology, Borel sets and coordinate observables [fdip-004C]AGENTDRAFTED
- October 31, 2026
On the four-cycle, a configuration is a point \(x=(x_0,x_1,x_2,x_3)\in \mathbb R^4\). The product topology makes \((-1,1)^4\) open. The Borel sigma-algebra also contains the closed half-space \(H=\{x:x_0\le 0\}\), because its complement is open. Thus Borel sets include both open and closed coordinate conditions.
The coordinate observable \(p_0(x)=x_0\) is continuous: the preimage of an open interval is its coordinate cylinder. For every Borel \(A\subseteq \mathbb R\), the set \(p_0^{-1}(A)\) is Borel by the coordinate-product definition and Proposition 3, proving measurability. The indicator \(\mathbf 1_H\) is also measurable: its preimage of a Borel set is one of \(\varnothing ,H,H^c,\mathbb R^4\). It is not continuous at the origin, since its values on \((1/k,0,0,0)\), for positive integers \(k\), are all zero while its value at their limit is one.
Mathlib's continuous_apply and
measurable_pi_apply give the coordinate projection facts
for product topologies and product measurable spaces, respectively.
These deductions distinguish topology, measurable sets and measurable maps using the conventions of [tao2011measure, Definitions 1.4.16 and 1.4.32, pp. 87 and 95, preliminary version]. They say nothing by themselves about integrability. For example, the constant observable \(1\) is measurable, but its integral against the coordinate reference measure on \(\mathbb R^4\) is infinite.
Proposition 6. Coordinate tests for measurable maps [fdip-002G]AGENTDRAFTED
- October 25, 2026
Proposition 6. Coordinate tests for measurable maps [fdip-002G]AGENTDRAFTED
- October 25, 2026
Let \(V\) be finite and \((Y,\mathcal T)\) a measurable space. A map \(f:Y\to X_V\) is measurable if and only if every map \(y\mapsto f(y)(v)\) to the Borel real line is measurable. Continuous maps between finite real field spaces are Borel measurable. In particular this holds for linear maps, coordinate restriction, zero extension and polynomial functions. Compare [tao2011measure, Exercise 1.4.29 and Remark 1.4.33, pp. 95-96, preliminary version].
Proof.
- October 25, 2026
Proof.
- October 25, 2026
Necessity follows by preimages of cylinders. For sufficiency, the sets \(A\subseteq X_V\) with \(f^{-1}(A)\in \mathcal T\) form a sigma-algebra containing the cylinders; use Proposition 3. For a continuous map, preimages of open sets are open. The same sigma-algebra argument extends this to all Borel sets. Linearity gives continuity by Definition 1; finite sums and products give the polynomial case.
For \(R\subseteq V\), restriction \(\rho _R:X_V\to X_R\) sends \(x\) to \(x|_R\). Zero extension \(\iota _R:X_R\to X_V\) is \(y\) on \(R\) and zero elsewhere. Both are linear and measurable, and \(\rho _R\iota _R=\operatorname {id}_{X_R}\). The reverse composite zeros the removed coordinates and need not be the identity. This is precisely the real polynomial pullback pair, now with its Borel structures; it is not a claim about preserving reference volume.
The product-measurability equivalence is
measurable_pi_iff; it concerns measurable products, without
asserting topology or integrability. For Borel spaces an inducing map
also detects measurability through composition, as in
Topology.IsInducing.measurable_comp_iff; no measurable
range is required. Neither statement attaches a state to every observable.
Definition 7. Coordinate Lebesgue reference measure [fdip-002H]AGENTDRAFTED
- October 25, 2026
Definition 7. Coordinate Lebesgue reference measure [fdip-002H]AGENTDRAFTED
- October 25, 2026
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.
Example 8. Volumes of four-coordinate boxes [fdip-004D]AGENTDRAFTED
- October 31, 2026
Example 8. Volumes of four-coordinate boxes [fdip-004D]AGENTDRAFTED
- October 31, 2026
Keep the four-cycle carrier \(V=\{0,1,2,3\}\). For real \(a_i\le b_i\), let \[B=\{x\in \mathbb R^4:a_i<x_i\le b_i\text { for }i=0,1,2,3\}.\] The coordinate Lebesgue measure gives \[\lambda _V(B)=\prod _{i=0}^3(b_i-a_i).\] Each factor is the length of its half-open interval, and the defining rectangle law multiplies them. If an endpoint pair is equal, the box is empty and the formula gives zero.
If every lower endpoint is zero and every upper endpoint is one, the box has volume \(1^4=1\). For lower endpoints \((0,0,-1,0)\) and upper endpoints \((2,1,1,3)\), its side lengths are \((2,1,2,3)\), so \[\lambda _V(B)=2\cdot 1\cdot 2\cdot 3=12.\] For \(a_i=-k\) and \(b_i=k\) in all 4 coordinates, with \(k>0\), the volume is \((2k)^4\). These volumes are unbounded as \(k\) increases, so the whole configuration space has infinite volume. Neither the edge weights nor a mass parameter enter these values. Reference volume is not a probability law; the later Gaussian density supplies a normalized weighting.
This is the rectangle formula of Definition 7, from
[tao2011measure, Proposition 1.7.11, pp. 197-199, preliminary version].
Mathlib's MeasureTheory.Measure.pi_pi gives the finite-product
rectangle law; Real.volume_Ioc gives each interval length.
Lemma 9. Uniqueness from finite rational cubes [fdip-002I]AGENTDRAFTED
- October 25, 2026
Lemma 9. Uniqueness from finite rational cubes [fdip-002I]AGENTDRAFTED
- October 25, 2026
Let \(V\) be finite. Suppose two Borel measures \(\mu ,\nu \) on \(X_V\) agree on all bounded half-open coordinate boxes with rational endpoints and on the empty set. Assume explicitly that their common mass on every rational cube \(C_k=\{x\in X_V:-k<x(v)\le k\text { for every }v\in V\}\), \(k\ge 1\), is finite. Then \(\mu =\nu \). In particular the hypothesis holds if both assign the prescribed finite Lebesgue volumes to those boxes. For empty \(V\), a box is the singleton, and agreement of its mass gives the conclusion.
Proof.
- October 25, 2026
Proof.
- October 25, 2026
For nonempty \(V\), these rational boxes together with the empty set form a pi-system: intersections are again such boxes or empty. Each rational open box is a countable union of half-open rational boxes contained in it, so this pi-system generates the Borel structure by Proposition 3. Fix \(k\). Restrict by \(\mu _k(A)=\mu (A\cap C_k)\) and \(\nu _k(A)=\nu (A\cap C_k)\). The restrictions are finite, have the same finite total mass, and agree on the generating boxes because intersection with \(C_k\) stays in that pi-system.
For completeness, the pi-lambda argument is as follows. A lambda-system contains the whole space and is closed under complements and disjoint countable unions. Let \(\mathcal D\) be the smallest lambda-system containing a pi-system \(\mathcal P\). For \(A\in \mathcal P\), the sets \(B\) satisfying \(A\cap B\in \mathcal D\) form a lambda-system: complement closure uses the difference of two nested members of \(\mathcal D\), and disjoint-union closure is immediate. It contains \(\mathcal P\), hence \(\mathcal D\). Repeating with fixed \(B\in \mathcal D\) shows that \(\mathcal D\) is closed under intersections. Complement and disjoint-union closure then give arbitrary countable unions by disjointification. Thus \(\mathcal D\) is a sigma-algebra.
The class on which \(\mu _k=\nu _k\) is a lambda-system: complements use subtraction from their equal finite total masses, and disjoint unions use countable additivity. It therefore contains every Borel set. Finally \(C_k\uparrow X_V\); continuity from below gives \(\mu (A)=\lim _k\mu _k(A)=\lim _k\nu _k(A)=\nu (A)\). No subtraction of infinite masses occurs.
This is the localized uniqueness argument behind
[tao2011measure, Proposition 1.7.11, pp. 197-199, preliminary version].
Mathlib's MeasureTheory.Measure.pi_eq characterizes a
sigma-finite product by all measurable rectangles. TauCeti's
MeasureTheory.Measure.ext_pi assumes a finite total
first measure; it cannot be applied directly to positive-dimensional
\(\lambda _V\). Bare agreement of arbitrary infinite measures on rational
boxes is not the lemma stated here.
Proposition 10. Reindexing and splitting reference volume [fdip-002J]AGENTDRAFTED
- October 25, 2026
Proposition 10. Reindexing and splitting reference volume [fdip-002J]AGENTDRAFTED
- October 25, 2026
For a bijection \(e:V\to W\), define \(U_e:X_V\to X_W\) by \((U_ex)(w)=x(e^{-1}w)\). It is a linear homeomorphism, with inverse \(U_{e^{-1}}\), preserving the counting pairing, and \[(U_e)_*\lambda _V=\lambda _W,\qquad f_*\mu (B):=\mu (f^{-1}B).\] For a disjoint decomposition \(V=R\sqcup D\), the restriction-pair map \(\sigma (x)=(x|_R,x|_D)\) has inverse pasting and satisfies \[\sigma _*\lambda _V=\lambda _R\otimes \lambda _D.\] Either factor may be empty, carrying singleton mass one.
Proof.
- October 25, 2026
Proof.
- October 25, 2026
The displayed maps and inverses are linear, hence continuous by Definition 1. Reindexing the finite sum proves preservation of \(h_V\). For a target rectangle \(\prod _wA_w\), its preimage under \(U_e\) is \(\prod _vA_{e(v)}\). The rectangle formula and reindexing of a finite product give equal measures. The same argument for \(\sigma \) combines the retained and removed coordinate boxes. The target generating boxes have prescribed finite cube masses, so Lemma 9 extends both equalities to all Borel sets.
An enumeration \(b:\{1,\ldots ,n\}\to V\) gives the chart \(C_b(x)_i=x(b(i))\). It therefore transports \(\lambda _V\) to ordinary Borel Lebesgue measure on \(\mathbb R^n\); two charts differ by a coordinate permutation. At \(n=0\) both spaces are singletons with mass one. This proves independence of enumeration without a determinant calculation.
These finite-coordinate proofs use the product convention of
[tao2011measure, Section 1.7.4, pp. 194-199, preliminary version].
The corresponding sigma-finite APIs are
MeasureTheory.measurePreserving_piCongrLeft and
MeasureTheory.measurePreserving_piEquivPiSubtypeProd; the latter
uses a decidable splitting predicate. A one-coordinate split is
TauCeti.measurePreserving_piSplitAt, and the specified
four-coordinate grouping is
TauCeti.measurePreserving_finFourArrowPairPair.
Bare restriction \(\rho _R\) is measurable, but if \(D\ne \varnothing \)
it is not reference-preserving: for a Borel \(A\subseteq X_R\) of finite
positive mass, \(\rho _R^{-1}(A)\) has mass
\(\lambda _R(A)\lambda _D(X_D)=\infty \). This includes \(R=\varnothing \),
when the target singleton has mass one. The probability-factor assumption
in TauCeti.measurePreserving_pi_comp_embedding excludes
these unnormalized Lebesgue factors. Normalized marginals are a different
measure statement.
Theorem 11. Linear changes of reference volume [fdip-002K]AGENTDRAFTED
- October 25, 2026
Theorem 11. Linear changes of reference volume [fdip-002K]AGENTDRAFTED
- October 25, 2026
Let \(T:X_V\to X_W\) be an invertible real linear map, with \(|V|=|W|=n\). Choose ordered indicator bases and normalized top forms \(\eta _V,\eta _W\), each taking value one on its chosen basis. Define \[T^*\eta _W=d(T)\eta _V,\qquad J(T)=|d(T)|.\] Reordering either basis changes \(d(T)\) only by a sign; \(J(T)>0\) is the reference-volume Jacobian. For Borel sets \(E,B\), \[\begin {aligned} \lambda _W(T(E))&=J(T)\lambda _V(E),\\ T_*\lambda _V(B)&=J(T)^{-1}\lambda _W(B). \end {aligned}\] For nonnegative Borel \(F:X_W\to [0,\infty ]\), \[\int _{X_V}F(Tx)\,d\lambda _V(x) =J(T)^{-1}\int _{X_W}F(y)\,d\lambda _W(y).\] For real signed \(F\), absolute integrability on either side is equivalent to that on the other; under this condition the same equality holds. Translation, and hence \(x\mapsto T(x)+b\), has the same coefficient.
For an endomorphism, \(d(T)=\det T\) only when source and target use the same normalized top form. Independently ordered indicator bases give \(d(T)=\varepsilon \det T\), \(\varepsilon \in \{1,-1\}\), although \(J(T)=|\det T|\). The identity on \(\mathbb R^2\) with reversed target order has \(d=-1\), intrinsic determinant \(1\), and \(J=1\). In dimension zero the top form is \(1\) and \(J=1\).
Proof.
- October 25, 2026
Proof.
- October 25, 2026
Top exterior powers are one-dimensional. For composable maps \(T,S\), use the same intermediate form to obtain \((ST)^*\eta =d(S)d(T)\eta _V\). Thus \(J(ST)=J(S)J(T)\); applying this to \(T^{-1}T\) gives \(J(T^{-1})=J(T)^{-1}\). The absolute identities are independent of enumeration. Since \(T^{-1}\) is continuous, \(T(E)\) is Borel.
On the Borel real line, translation preserves length and multiplication by \(a\ne 0\) has pushforward coefficient \(|a|^{-1}\). Compare preimages of bounded intervals and then use finite-on-bounded-interval uniqueness. When \(a<0\), the reversed half-open interval has the same length since singletons have measure zero. By rectangles and Lemma 9, scaling one coordinate has that coefficient. Coordinate permutations preserve measure by Proposition 10. With a common basis their signed top-form multipliers are \(a\) for scaling and \(-1\) for a swap.
For distinct coordinates \(i,j\), the shear \(E(x)=x+c\,x(j)\delta _i\) preserves volume. Split off coordinate \(i\), writing the others as \(z\). For fixed \(z\), translation invariance gives \[\int _{\mathbb R}F(z,t+c\,z(j))\,dt =\int _{\mathbb R}F(z,t)\,dt.\] Nonnegative Tonelli on the sigma-finite uncompleted Borel product then gives equality of full integrals; indicators give measure preservation. The shear's top-form multiplier is \(1\), since replacing the \(j\)th basis vector by \(\delta _j+c\delta _i\) leaves its top wedge unchanged. Tonelli here is [tao2011measure, Theorem 1.7.15, pp. 200-201, preliminary version], not the complete-space variant.
These elementary maps generate every isomorphism in indicator charts. Induct on \(n\), the zero-dimensional case being immediate. For \(n>0\), the image of the first basis vector is nonzero. Swap target coordinates to put a nonzero coefficient first, scale it to one, and subtract its suitable multiples from the other target coordinates. The resulting map \(ET\) sends the first domain basis vector to the first target one. If the first coefficient of \((ET)e_j\) is \(a_j\) for \(j>1\), precompose with the domain shears \(e_j\mapsto e_j-a_je_1\). The resulting map fixes the first basis vector and maps the complementary span into the target complementary span. Its restriction is injective; it is surjective because the first coefficient of a preimage of a complementary vector must be zero. Induction on these complements, extending their elementary maps by identity on the first coordinate, completes the factorization.
Pushforwards compose and commute with scalar multiplication of measures. Multiplying the elementary coefficients therefore proves \(T_*\lambda _V=J(T)^{-1}\lambda _W\), after the measure-preserving coordinate charts of Proposition 10. Substituting \(B=T(E)\) gives the image formula. Translations in several coordinates follow from the one-dimensional result and rectangles, yielding the affine assertion. No reciprocal formula is asserted for a singular map.
The integral formula follows first for indicators from the measure identity, then for nonnegative simple functions by additivity, then by increasing simple approximation and monotone convergence. Apply it to \(|F|\) to obtain absolute-integrability equivalence, since \(J(T)\) is positive and finite. Only then apply it to \(F^+,F^-\) and subtract. No multiplication closure of \(L^1\) is used.
The image convention is stated in
[tao2011measure, Exercises 1.2.20-1.2.22, p. 41, preliminary version];
the argument above proves its finite-field form. Mathlib's
Real.map_linearMap_volume_pi_eq_smul_volume_pi is a
finite-coordinate endomorphism theorem with nonzero determinant and
reciprocal pushforward coefficient. Distinct carriers require the
coordinate transport already proved, not an intrinsic signed determinant
between unrelated spaces.
Corollary 12. Counting isometries preserve volume [fdip-002L]AGENTDRAFTED
- October 25, 2026
Corollary 12. Counting isometries preserve volume [fdip-002L]AGENTDRAFTED
- October 25, 2026
A linear isomorphism \(T:X_V\to X_W\) preserving the counting inner products satisfies \(J(T)=1\). It therefore preserves coordinate Lebesgue measure and the integrals in Theorem 11. An isometric embedding into a higher-dimensional space is not included.
Proof.
- October 25, 2026
Proof.
- October 25, 2026
The vectors \(T\delta _v\) form an orthonormal basis. On simple top exterior vectors the induced inner product is \[\left \langle u_1\wedge \cdots \wedge u_n, v_1\wedge \cdots \wedge v_n\right \rangle =\det \bigl (h(u_i,v_j)\bigr ).\] Alternating multilinearity makes this well-defined on the top exterior power. The wedge of an ordered orthonormal basis has squared norm one, and an isometry preserves every entry of the displayed Gram matrix. Consequently \(d(T)^2=1\), so \(J(T)=1\); apply Theorem 11. The empty wedge also has norm one.
This is a direct consequence of the preceding transformation theorem,
with the convention of
[tao2011measure, Exercise 1.2.21, p. 41, preliminary version].
Mathlib's LinearIsometryEquiv.measurePreserving concerns
finite-dimensional real inner-product spaces with compatible Borel
structures and their canonical volumes. An arbitrary perfect pairing
or a general quadratic-form isometry does not supply these hypotheses.
Definition 13. Induced Euclidean volume on a subspace [fdip-002M]AGENTDRAFTED
- October 25, 2026
Definition 13. Induced Euclidean volume on a subspace [fdip-002M]AGENTDRAFTED
- October 25, 2026
Let \(H\) be a finite-dimensional real inner-product space, in particular a subspace of \((X_V,h_V)\) with its induced topology and inner product. Choose an orthonormal chart \(C:H\to \mathbb R^k\). The induced Euclidean measure is \(\lambda _H=(C^{-1})_*\lambda _{\{1,\ldots ,k\}}\) on its Borel sets. It is independent of the orthonormal chart. If \(H=\{0\}\), it is unit mass at zero. For an affine translate \(a+H\), use the pushforward of \(\lambda _H\) under \(h\mapsto a+h\).
Proof.
- October 25, 2026
Proof.
- October 25, 2026
A finite Gram-Schmidt construction produces an orthonormal basis: normalize a nonzero vector by its positive norm, subtract its components from a spanning family, and continue in the orthogonal complement. Positivity permits normalization at each nonzero step. Two such charts differ by a linear isometric isomorphism of \(\mathbb R^k\); Corollary 12 proves independence. A different choice of origin in \(a+H\) differs by a translation in \(H\), which preserves its coordinate measure by Theorem 11.
For a proper linear subspace \(H\subsetneq X_V\), extend its orthonormal basis to one of \(X_V\) by the same construction. In those coordinates \(H\) lies in a coordinate hyperplane and is closed. Within each bounded cube that hyperplane has measure zero: the rectangle formula has a zero-measure singleton factor and finite other factors. Monotonicity and countable exhaustion give zero ambient measure; orthogonal invariance transports this back. But the unit coordinate cube in \(H\) has induced mass one. Thus induced volume is not the restriction of ambient \(\lambda _V\).
For example, on \(H=\{(s,s):s\in \mathbb R\}\), the segment \(0\le s\le 1\) has induced length \(\sqrt 2\), ambient area zero, and raw \(s\)-coordinate length one. Indeed its unit vector is \((1,1)/\sqrt 2\), so its orthonormal coordinate runs from zero to \(\sqrt 2\). An arbitrary basis therefore needs its volume factor.
The argument uses the transformation convention of
[tao2011measure, Exercise 1.2.21, p. 41, preliminary version].
Mathlib's OrthonormalBasis.measurePreserving_repr targets
EuclideanSpace; PiLp.volume_preserving_ofLp and
PiLp.volume_preserving_toLp identify its real finite PiLp
volume with ordinary coordinate products. TauCeti's
Module.Basis.volume_eq_smul_addHaar records the
square-root Gram determinant factor for an arbitrary basis, while
AffineIsometryEquiv.measurePreserving applies to
finite-dimensional real Borel inner-product spaces. These compare the
same canonical-volume convention.
Example 14. Image volume and pushforward mass [fdip-002N]AGENTDRAFTED
- October 25, 2026
Example 14. Image volume and pushforward mass [fdip-002N]AGENTDRAFTED
- October 25, 2026
On the Borel real line, let \(T(x)=2x\). The
Jacobian theorem gives \(J(T)=2\), but its two measure
directions have reciprocal coefficients:
\[\lambda _{\mathbb R}(T[0,1])=2,\qquad
T_*\lambda _{\mathbb R}([0,1])=\tfrac 12.\]
The first set is \([0,2]\), whereas the second expression measures the
preimage \([0,1/2]\). This directly checks the convention of
[tao2011measure, Exercise 1.2.21, p. 41, preliminary version].
Mathlib's Real.map_volume_mul_left requires a nonzero scalar
and gives the reciprocal absolute pushforward factor.
Put \(q_V(x)=x^2\) and \(q_W(y)=y^2/4\). Then \(q_W(Tx)=q_V(x)\) although \(J(T)=2\). Preserving a quadratic form alone does not preserve the supplied reference volume.
If a Borel weight \(w\ge 0\) has a finite positive integral \(Z=\int w\,d\lambda _V\), replacing the reference by \(c\lambda _V\), \(c>0\), replaces \(Z\) by \(cZ\). Consequently \((cZ)^{-1}w\,d(c\lambda _V)=Z^{-1}w\,d\lambda _V\). This conditional cancellation follows from linearity for indicators, simple functions and monotone limits. It proves neither existence nor finiteness of \(Z\); the reference and the action are separate data.
Lemma 15. Orthogonal sums have product volume [fdip-002Q]AGENTDRAFTED
- October 25, 2026
Lemma 15. Orthogonal sums have product volume [fdip-002Q]AGENTDRAFTED
- October 25, 2026
Let \(E=E_1\mathbin \perp E_2\) be an orthogonal direct sum of finite-dimensional real inner-product spaces. Use their canonical Euclidean volumes on the uncompleted Borel sigma-algebras. Addition \(a(x_1,x_2)=x_1+x_2\) is a measure-preserving isometric isomorphism: \[a_*(\lambda _{E_1}\otimes \lambda _{E_2})=\lambda _E.\] All these measures are sigma-finite. Nonnegative Borel functions therefore satisfy Tonelli's iterated-integral identities. For a real Borel function with finite absolute integral, Fubini holds and its sections are integrable almost everywhere.
Proof.
- October 25, 2026
Proof.
- October 25, 2026
Concatenate orthonormal bases of \(E_1\) and \(E_2\). The resulting orthonormal chart of \(E\) turns addition into concatenation of coordinate tuples. The finite product splitting identifies the measures, and chart independence is already proved at Definition 13. Empty bases give singleton factors of mass one, so the argument includes zero summands.
Each finite chart is exhausted by cubes \([-N,N]^n\) of finite measure; in dimension zero the whole measure has mass one. Thus [tao2011measure, Theorem 1.7.15, pp. 200-201, preliminary version] applies to these uncompleted sigma-finite products. Applying Tonelli to the absolute value shows that section integrals of the absolute value are finite almost everywhere. Applying it to positive and negative parts then gives signed Fubini. The null-section statement in [tao2011measure, Corollary 1.7.17, pp. 201-202, preliminary version] concerns product-null sets; it does not remove the absolute-integrability hypothesis for signed integrals.
This follows from canonical Euclidean volume and finite product splitting.
Mathlib's LinearIsometryEquiv.measurePreserving supports the
isometry step for finite-dimensional real Borel inner-product spaces with
canonical volume; arbitrary perfect pairings do not supply these hypotheses.