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
measure 1 to the parallelepiped spanned by any orthonormal basis, and that it coincides with
the canonical volume from the MeasureSpace 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_volumeForm_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.
The Haar measure defined by any orthonormal basis of a finite-dimensional inner product space is equal to its volume measure.
An orthonormal basis of a finite-dimensional inner product space defines a measurable equivalence between the space and the Euclidean space of the same dimension.
Equations
Instances For
The measurable equivalence defined by an orthonormal basis is volume preserving.
The measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving.
A copy of EuclideanSpace.volume_preserving_measurableEquiv for the canonical spelling of the
equivalence.
The reverse direction of PiLp.volume_preserving_measurableEquiv, since
MeasurePreserving.symm only works for MeasurableEquivs.
Every linear isometry on a real finite dimensional Hilbert space is measure-preserving.
Every linear isometry equivalence is a measurable equivalence.
Equations
- LinearIsometryEquiv.toMeasureEquiv f = { toEquiv := ↑f, measurable_toFun := (_ : Measurable ⇑f), measurable_invFun := (_ : Measurable ⇑(LinearIsometryEquiv.symm f)) }