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.

def LinearIsometryEquiv.toMeasureEquiv {E : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] (f : E ≃ₗᵢ[ℝ] F) : E ≃ᵐ F

Every linear isometry equivalence is a measurable equivalence.

Equations

• f.toMeasureEquiv = { toEquiv := ↑f, measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem LinearIsometryEquiv.coe_toMeasureEquiv {E : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] (f : E ≃ₗᵢ[ℝ] F) : ⇑f.toMeasureEquiv = ⇑f

theorem LinearIsometryEquiv.toMeasureEquiv_symm {E : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] (f : E ≃ₗᵢ[ℝ] F) : f.toMeasureEquiv.symm = f.symm.toMeasureEquiv

theorem Orientation.measure_orthonormalBasis {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [Fintype ι] [FiniteDimensional ℝ F] {n : ℕ} [_i : Fact (Module.finrank ℝ F = n)] (o : Orientation ℝ F (Fin n)) (b : OrthonormalBasis ι ℝ F) : o.volumeForm.measure (parallelepiped ⇑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_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] {n : ℕ} [_i : Fact (Module.finrank ℝ F = n)] (o : Orientation ℝ F (Fin n)) : o.volumeForm.measure = 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_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [Fintype ι] [FiniteDimensional ℝ F] (b : OrthonormalBasis ι ℝ F) : MeasureTheory.volume (parallelepiped ⇑b) = 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_4} {F : Type u_5} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (b : OrthonormalBasis ι ℝ F) : b.toBasis.addHaar = MeasureTheory.volume

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

noncomputable def OrthonormalBasis.measurableEquiv {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [Fintype ι] (b : OrthonormalBasis ι ℝ F) : F ≃ᵐ EuclideanSpace ℝ ι

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

• b.measurableEquiv = b.repr.toHomeomorph.toMeasurableEquiv

theorem OrthonormalBasis.measurePreserving_measurableEquiv {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [Fintype ι] [FiniteDimensional ℝ F] (b : OrthonormalBasis ι ℝ F) : MeasureTheory.MeasurePreserving (⇑b.measurableEquiv) MeasureTheory.volume MeasureTheory.volume

The measurable equivalence defined by an orthonormal basis is volume preserving.

theorem OrthonormalBasis.measurePreserving_repr {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [Fintype ι] [FiniteDimensional ℝ F] (b : OrthonormalBasis ι ℝ F) : MeasureTheory.MeasurePreserving (⇑b.repr) MeasureTheory.volume MeasureTheory.volume

theorem OrthonormalBasis.measurePreserving_repr_symm {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [Fintype ι] [FiniteDimensional ℝ F] (b : OrthonormalBasis ι ℝ F) : MeasureTheory.MeasurePreserving (⇑b.repr.symm) MeasureTheory.volume MeasureTheory.volume

theorem EuclideanSpace.volume_preserving_measurableEquiv (ι : Type u_4) [Fintype ι] : MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) MeasureTheory.volume MeasureTheory.volume

The measure equivalence between EuclideanSpace ℝ ι and ι → ℝ is volume preserving.

theorem PiLp.volume_preserving_equiv (ι : Type u_4) [Fintype ι] : MeasureTheory.MeasurePreserving (⇑(WithLp.equiv 2 (ι → ℝ))) MeasureTheory.volume MeasureTheory.volume

A copy of EuclideanSpace.volume_preserving_measurableEquiv for the canonical spelling of the equivalence.

theorem PiLp.volume_preserving_equiv_symm (ι : Type u_4) [Fintype ι] : MeasureTheory.MeasurePreserving (⇑(WithLp.equiv 2 (ι → ℝ)).symm) MeasureTheory.volume MeasureTheory.volume

The reverse direction of PiLp.volume_preserving_measurableEquiv, since MeasurePreserving.symm only works for MeasurableEquivs.

theorem volume_euclideanSpace_eq_dirac (ι : Type u_4) [Fintype ι] [IsEmpty ι] : MeasureTheory.volume = MeasureTheory.Measure.dirac 0

theorem LinearIsometryEquiv.measurePreserving {E : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (f : E ≃ₗᵢ[ℝ] F) : MeasureTheory.MeasurePreserving (⇑f) MeasureTheory.volume MeasureTheory.volume

Every linear isometry on a real finite dimensional Hilbert space is measure-preserving.