mathlib3 documentation

measure_theory.measure.haar.inner_product_space

Volume forms and measures on inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measure 1 to the parallelepiped spanned by any orthonormal basis, and that it coincides with the canonical volume from the measure_space instance.

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.