Volume forms and measures on inner product spaces #
A volume form induces a Lebesgue measure on general finite-dimensional real vector spaces. In this
file, we discuss the specific situation of inner product spaces, where an orientation gives
rise to a canonical volume form. We show that the measure coming from this volume form gives
1 to the parallelepiped spanned by any orthonormal basis, and that it coincides with
volume from the
The volume form coming from an orientation in an inner product space gives measure
1 to the
parallelepiped associated to any orthonormal basis. This is a rephrasing of
abs_volume_form_apply_of_orthonormal in terms of measures.
In an oriented inner product space, the measure coming from the canonical volume form associated to an orientation coincides with the volume.
The volume measure in a finite-dimensional inner product space gives measure
1 to the
parallelepiped spanned by any orthonormal basis.