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

source
def LinearIsometryEquiv.toMeasurableEquiv {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.toMeasurableEquiv = { toEquiv := ↑f, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
@[simp]
theorem LinearIsometryEquiv.coe_toMeasurableEquiv {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.toMeasurableEquiv = ⇑f
source
@[simp]
theorem LinearIsometryEquiv.toMeasurableEquiv_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.symm.toMeasurableEquiv = f.toMeasurableEquiv.symm
source
@[simp]
theorem LinearIsometryEquiv.coe_symm_toMeasurableEquiv {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.toMeasurableEquiv.symm = ⇑f.symm
source
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.

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

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

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

source
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

Instances For

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

source
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
source
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
source
@[deprecated MeasurableEquiv.toLp (since := "2025-11-02")]
def EuclideanSpace.measurableEquiv (ι : Type u_4) :
EuclideanSpace ℝ ι ≃ᵐ (ι → ℝ)

`WithLp.equiv` as a `MeasurableEquiv`.

Equations

- EuclideanSpace.measurableEquiv ι = (MeasurableEquiv.toLp 2 (ι → ℝ)).symm

Instances For

source
@[deprecated MeasurableEquiv.coe_toLp (since := "2025-11-02")]
theorem EuclideanSpace.measurableEquiv_toEquiv (ι : Type u_4) :
(EuclideanSpace.measurableEquiv ι).toEquiv = WithLp.equiv 2 (ι → ℝ)
source
@[deprecated MeasurableEquiv.coe_toLp (since := "2025-11-02")]
theorem EuclideanSpace.coe_measurableEquiv (ι : Type u_4) :
⇑(EuclideanSpace.measurableEquiv ι) = WithLp.ofLp
source
@[deprecated MeasurableEquiv.coe_toLp_symm (since := "2025-11-02")]
theorem EuclideanSpace.coe_measurableEquiv_symm (ι : Type u_4) :
⇑(EuclideanSpace.measurableEquiv ι).symm = WithLp.toLp 2
source
theorem EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp (ι : Type u_4) [Fintype ι] :
MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) MeasureTheory.volume MeasureTheory.volume

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

source
@[deprecated EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp (since := "2025-07-26")]
theorem EuclideanSpace.volume_preserving_measurableEquiv (ι : Type u_4) [Fintype ι] :
MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) MeasureTheory.volume MeasureTheory.volume

Alias of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`.

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

source
theorem PiLp.volume_preserving_ofLp (ι : Type u_4) [Fintype ι] :
MeasureTheory.MeasurePreserving WithLp.ofLp MeasureTheory.volume MeasureTheory.volume

A copy of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp` for the canonical spelling of the equivalence.

source
theorem PiLp.volume_preserving_toLp (ι : Type u_4) [Fintype ι] :
MeasureTheory.MeasurePreserving (WithLp.toLp 2) MeasureTheory.volume MeasureTheory.volume

The reverse direction of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, since `MeasurePreserving.symm` only works for `MeasurableEquiv`s.

source
theorem volume_euclideanSpace_eq_dirac (ι : Type u_4) [Fintype ι] [IsEmpty ι] :
MeasureTheory.volume = MeasureTheory.Measure.dirac 0
source
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.