# Documentation

Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

# 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.

theorem Orientation.measure_orthonormalBasis {ι : Type u_1} {F : Type u_2} [] [] [] [] [] {n : } [_i : Fact ()] (o : Orientation F (Fin n)) (b : ) :
= 1

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.

theorem Orientation.measure_eq_volume {F : Type u_2} [] [] [] [] {n : } [_i : Fact ()] (o : Orientation F (Fin n)) :
= MeasureTheory.volume

In an oriented inner product space, the measure coming from the canonical volume form associated to an orientation coincides with the volume.

theorem OrthonormalBasis.volume_parallelepiped {ι : Type u_1} {F : Type u_2} [] [] [] [] [] (b : ) :
MeasureTheory.volume () = 1

The volume measure in a finite-dimensional inner product space gives measure 1 to the parallelepiped spanned by any orthonormal basis.

theorem OrthonormalBasis.addHaar_eq_volume {ι : Type u_3} {F : Type u_4} [] [] [] [] [] (b : ) :
= MeasureTheory.volume

The Haar measure defined by any orthonormal basis of a finite-dimensional inner product space is equal to its volume measure.

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.