mathlib3 documentation

measure_theory.measure.haar.of_basis

Additive Haar measure constructed from a basis #

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

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 ι] [add_comm_group E] [module ℝ E] (v : ι → 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

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

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

@[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.

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

theorem parallelepiped_eq_sum_segment {ι : Type u_1} {E : Type u_3} [fintype ι] [add_comm_group E] [module ℝ E] (v : ι → E) :

parallelepiped v = finset.univ.sum (λ (i : ι), segment ℝ 0 (v i))

theorem convex_parallelepiped {ι : Type u_1} {E : Type u_3} [fintype ι] [add_comm_group E] [module ℝ E] (v : ι → E) :

convex ℝ (parallelepiped v)

theorem parallelepiped_eq_convex_hull {ι : Type u_1} {E : Type u_3} [fintype ι] [add_comm_group E] [module ℝ E] (v : ι → E) :

parallelepiped v = ⇑(convex_hull ℝ) (finset.univ.sum (λ (i : ι), {0, v i}))

A parallelepiped is the convex hull of its vertices

theorem parallelepiped_single {ι : Type u_1} [fintype ι] [decidable_eq ι] (a : ι → ℝ) :

parallelepiped (λ (i : ι), pi.single i (a i)) = set.uIcc 0 a

The axis aligned parallelepiped over ι → ℝ is a cuboid.

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' := _}

@[simp]

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

↑(b.parallelepiped) = parallelepiped ⇑b

@[simp]

theorem basis.parallelepiped_reindex {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [fintype ι] [fintype ι'] [normed_add_comm_group E] [normed_space ℝ E] (b : basis ι ℝ E) (e : ι ≃ ι') :

(b.reindex e).parallelepiped = b.parallelepiped

theorem basis.parallelepiped_map {ι : Type u_1} {E : Type u_3} {F : Type u_4} [fintype ι] [normed_add_comm_group E] [normed_add_comm_group F] [normed_space ℝ E] [normed_space ℝ F] (b : basis ι ℝ E) (e : E ≃ₗ[ℝ ] F) :

(b.map e).parallelepiped = topological_space.positive_compacts.map ⇑e _ _ b.parallelepiped

@[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

@[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

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

@[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}

@[protected, instance]

noncomputable def real.measure_space :

measure_theory.measure_space ℝ

Equations

real.measure_space = measure_space_of_inner_product_space

Miscellaneous instances for `euclidean_space` #

In combination with measure_space_of_inner_product_space, these put a measure_space structure on euclidean_space.

@[protected, instance]

def euclidean_space.measurable_space (ι : Type u_1) [fintype ι] :

measurable_space (euclidean_space ℝ ι)

Equations

euclidean_space.measurable_space ι = measurable_space.pi

@[protected, instance]

def euclidean_space.borel_space (ι : Type u_1) [fintype ι] :

borel_space (euclidean_space ℝ ι)

@[simp]

theorem euclidean_space.measurable_equiv_to_equiv (ι : Type u_1) [fintype ι] :

(euclidean_space.measurable_equiv ι).to_equiv = pi_Lp.equiv 2 (λ (i : ι), ℝ)

@[protected]

noncomputable def euclidean_space.measurable_equiv (ι : Type u_1) [fintype ι] :

euclidean_space ℝ ι ≃ᵐ (ι → ℝ)

pi_Lp.equiv as a measurable_equiv.

Equations

euclidean_space.measurable_equiv ι = {to_equiv := pi_Lp.equiv 2 (λ (i : ι), ℝ), measurable_to_fun := _, measurable_inv_fun := _}

theorem euclidean_space.coe_measurable_equiv (ι : Type u_1) [fintype ι] :

⇑(euclidean_space.measurable_equiv ι) = ⇑(pi_Lp.equiv 2 (λ (i : ι), ℝ))