mathlib documentation


Additive Haar measure constructed from a basis #

Given a basis of a finite-dimensional real vector space, we define the corresponding Lebesgue measure, which gives measure 1 to the parallelepiped spanned by the basis.

Main definitions #

In particular, we declare a measure_space instance on any finite-dimensional inner product space, by using the Lebesgue measure associated to some orthonormal basis (which is in fact independent of the basis).

def parallelepiped {ι : Type u_1} {E : Type u_3} [fintype ι] [add_comm_group E] [module E] (v : ι E) :
set E

The closed parallelepiped spanned by a finite family of vectors.

theorem mem_parallelepiped_iff {ι : Type u_1} {E : Type u_3} [fintype ι] [add_comm_group E] [module E] (v : ι E) (x : E) :
x parallelepiped v (t : ι ) (ht : t set.Icc 0 1), x = finset.univ.sum (λ (i : ι), t i v i)
theorem image_parallelepiped {ι : Type u_1} {E : Type u_3} {F : Type u_4} [fintype ι] [add_comm_group E] [module E] [add_comm_group F] [module F] (f : E →ₗ[] F) (v : ι E) :
theorem parallelepiped_comp_equiv {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [fintype ι] [fintype ι'] [add_comm_group E] [module E] (v : ι E) (e : ι' ι) :

Reindexing a family of vectors does not change their parallelepiped.

The parallelepiped spanned by a basis, as a compact set with nonempty interior.

noncomputable def basis.add_haar {ι : Type u_1} {E : Type u_3} [fintype ι] [normed_add_comm_group E] [normed_space E] [measurable_space E] [borel_space E] (b : basis ι E) :

The Lebesgue measure associated to a basis, giving measure 1 to the parallelepiped spanned by the basis.

Instances for basis.add_haar
@[protected, instance]

A finite dimensional inner product space has a canonical measure, the Lebesgue measure giving volume 1 to the parallelepiped spanned by any orthonormal basis. We define the measure using some arbitrary choice of orthonormal basis. The fact that it works with any orthonormal basis is proved in orthonormal_basis.volume_parallelepiped.