Commit 2022-12-13 06:33 f721cdca
View on Github →feat(measure_theory/measure/haar_lebesgue): Lebesgue measure coming from an alternating map (#17583)
To an n
-alternating form ω
on an n
-dimensional space, we associate a Lebesgue measure ω.measure
. We show that it satisfies ω.measure (parallelepiped v) = |ω v|
when v
is a family of n
vectors, where parallelepiped v
is the parallelepiped spanned by these vectors.
In the special case of inner product spaces, this gives a canonical measure when one takes for the alternating form the canonical one associated to some orientation. Therefore, we register a measure_space
instance on finite-dimensional inner product spaces. As the real line is a special case of inner product space, we need to redefine the Lebesgue measure there to avoid having two competing measure_space
instances.