Lemma. Orthogonal sums have product volume [fdip-002Q]

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.

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.