Volume forms and measures on inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measure_space instance.

source

theorem orientation.measure_orthonormal_basis {ι : Type u_1} {F : Type u_2} [fintype ι] [normed_add_comm_group F] [inner_product_space ℝ F] [finite_dimensional ℝ F] [measurable_space F] [borel_space F] {n : ℕ} [fact (fdim F = n)] (o : orientation ℝ F (fin n)) (b : orthonormal_basis ι ℝ F) :

⇑(o.volume_form.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_volume_form_apply_of_orthonormal in terms of measures.

source

theorem orientation.measure_eq_volume {F : Type u_2} [normed_add_comm_group F] [inner_product_space ℝ F] [finite_dimensional ℝ F] [measurable_space F] [borel_space F] {n : ℕ} [fact (fdim F = n)] (o : orientation ℝ F (fin n)) :

o.volume_form.measure = measure_theory.measure_space.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 orthonormal_basis.volume_parallelepiped {ι : Type u_1} {F : Type u_2} [fintype ι] [normed_add_comm_group F] [inner_product_space ℝ F] [finite_dimensional ℝ F] [measurable_space F] [borel_space F] (b : orthonormal_basis ι ℝ F) :

⇑measure_theory.measure_space.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.