Definition. Induced Euclidean volume on a subspace [fdip-002M]

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\).

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.