The volume of a parallelepiped and the Gram determinant

In a finite-dimensional real inner product space, the volume measure gives measure one to the parallelepiped spanned by an orthonormal basis (OrthonormalBasis.volume_parallelepiped). For an arbitrary family v of as many vectors as the dimension, the parallelepiped it spans has volume √(det G), where G is the Gram matrix ⟪vᵢ, vⱼ⟫ of v; both sides vanish when v is linearly dependent. For a basis b this says that the volume measure is √(det G) times the additive Haar measure b.addHaar normalized by b.

This converts integrals against a basis-normalized Haar measure, such as the coordinate measure in which a Riemannian volume density is expressed, into integrals against the volume measure.

Main results

• TauCeti.volume_parallelepiped: the parallelepiped spanned by v has volume √(det G).
• Module.Basis.volume_eq_smul_addHaar: the volume measure is √(det G) • b.addHaar.

References

• F. R. Gantmacher, The Theory of Matrices, Vol. 1, Chelsea, 1959, Chapter IX, §5 (the Gram determinant as the squared volume of a parallelepiped).

theorem TauCeti.volume_parallelepiped {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : ι → E) (hv : Fintype.card ι = Module.finrank ℝ E) : MeasureTheory.volume (parallelepiped v) = ENNReal.ofReal √(Matrix.gram ℝ v).det

In a finite-dimensional real inner product space, the parallelepiped spanned by a family of as many vectors as the dimension has volume the square root of the Gram determinant of the family.

theorem Module.Basis.volume_eq_smul_addHaar {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) : MeasureTheory.volume = ENNReal.ofReal √(Matrix.gram ℝ ⇑b).det • b.addHaar

The volume measure of a finite-dimensional real inner product space is the additive Haar measure normalized by a basis b, scaled by the square root of the Gram determinant of b.