# mathlibdocumentation

measure_theory.measure.haar_of_basis

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

• parallelepiped v is the parallelepiped spanned by a finite family of vectors.
• basis.parallelepiped is the parallelepiped associated to a basis, seen as a compact set with nonempty interior.
• basis.add_haar is the Lebesgue measure associated to a basis, giving measure 1 to the corresponding parallelepiped.

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 ι] [ E] (v : ι E) :
set E

The closed parallelepiped spanned by a finite family of vectors.

Equations
theorem mem_parallelepiped_iff {ι : Type u_1} {E : Type u_3} [fintype ι] [ E] (v : ι E) (x : E) :
(t : ι ) (ht : t 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 ι] [ E] [ F] (f : E →ₗ[] F) (v : ι E) :
@[simp]
theorem parallelepiped_comp_equiv {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [fintype ι] [fintype ι'] [ E] (v : ι E) (e : ι' ι) :

Reindexing a family of vectors does not change their parallelepiped.

theorem parallelepiped_orthonormal_basis_one_dim {ι : Type u_1} [fintype ι] (b : ) :
= 1 = set.Icc (-1) 0
def basis.parallelepiped {ι : Type u_1} {E : Type u_3} [fintype ι] [ E] (b : E) :

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

Equations
@[irreducible]
noncomputable def basis.add_haar {ι : Type u_1} {E : Type u_3} [fintype ι] [ E] [borel_space E] (b : E) :

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

Equations
Instances for basis.add_haar
@[protected, instance]
def is_add_haar_measure_basis_add_haar {ι : Type u_1} {E : Type u_3} [fintype ι] [ E] [borel_space E] (b : E) :
theorem basis.add_haar_self {ι : Type u_1} {E : Type u_3} [fintype ι] [ E] [borel_space E] (b : E) :
@[protected, instance]
noncomputable def measure_space_of_inner_product_space {E : Type u_3} [borel_space E] :

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.

Equations
@[protected, instance]
noncomputable def real.measure_space  :
Equations