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

source

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.

Equations

parallelepiped v = (λ (t : ι → ℝ), finset.univ.sum (λ (i : ι), t i • v i)) '' set.Icc 0 1

source

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)

source

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) :

⇑f '' parallelepiped v = parallelepiped (⇑f ∘ v)

source

@[simp]

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 : ι' ≃ ι) :

parallelepiped (v ∘ ⇑e) = parallelepiped v

Reindexing a family of vectors does not change their parallelepiped.

source

theorem parallelepiped_orthonormal_basis_one_dim {ι : Type u_1} [fintype ι] (b : orthonormal_basis ι ℝ ℝ) :

parallelepiped ⇑b = set.Icc 0 1 ∨ parallelepiped ⇑b = set.Icc (-1) 0

source

def basis.parallelepiped {ι : Type u_1} {E : Type u_3} [fintype ι] [normed_add_comm_group E] [normed_space ℝ E] (b : basis ι ℝ E) :

topological_space.positive_compacts E

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

Equations

b.parallelepiped = {to_compacts := {carrier := parallelepiped ⇑b, is_compact' := _}, interior_nonempty' := _}

source

@[irreducible]

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) :

measure_theory.measure E

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

Equations

b.add_haar = measure_theory.measure.add_haar_measure b.parallelepiped

Instances for basis.add_haar

is_add_haar_measure_basis_add_haar

source

@[protected, instance]

def is_add_haar_measure_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) :

b.add_haar.is_add_haar_measure

source

theorem basis.add_haar_self {ι : 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) :

⇑(b.add_haar) (parallelepiped ⇑b) = 1

source

@[protected, instance]

noncomputable def measure_space_of_inner_product_space {E : Type u_3} [normed_add_comm_group E] [inner_product_space ℝ E] [finite_dimensional ℝ E] [measurable_space E] [borel_space E] :

measure_theory.measure_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

measure_space_of_inner_product_space = {to_measurable_space := _inst_6, volume := (std_orthonormal_basis ℝ E).to_basis.add_haar}

source

@[protected, instance]

noncomputable def real.measure_space :

measure_theory.measure_space ℝ

Equations

real.measure_space = measure_space_of_inner_product_space