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.addHaar is the Lebesgue measure associated to a basis, giving measure 1 to the corresponding parallelepiped.

In particular, we declare a MeasureSpace 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 ι] [AddCommGroup E] [Module ℝ E] (v : ι → E) : Set E

The closed parallelepiped spanned by a finite family of vectors.

Equations

• parallelepiped v = (fun (t : ι → ℝ) => ∑ i : ι, t i • v i) '' Set.Icc 0 1

theorem mem_parallelepiped_iff {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] (v : ι → E) (x : E) : x ∈ parallelepiped v ↔ ∃ t ∈ Set.Icc 0 1, x = ∑ i : ι, t i • v i

theorem parallelepiped_basis_eq {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] (b : Basis ι ℝ E) : parallelepiped ⇑b = {x : E | ∀ (i : ι), (b.repr x) i ∈ Set.Icc 0 1}

theorem image_parallelepiped {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [AddCommGroup E] [Module ℝ E] [AddCommGroup 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 ι'] [AddCommGroup E] [Module ℝ E] (v : ι → E) (e : ι' ≃ ι) : parallelepiped (v ∘ ⇑e) = parallelepiped v

Reindexing a family of vectors does not change their parallelepiped.

theorem parallelepiped_orthonormalBasis_one_dim {ι : Type u_1} [Fintype ι] (b : OrthonormalBasis ι ℝ ℝ) : 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 ι] [AddCommGroup E] [Module ℝ E] (v : ι → E) : parallelepiped v = ∑ i : ι, segment ℝ 0 (v i)

theorem convex_parallelepiped {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] (v : ι → E) : Convex ℝ (parallelepiped v)

theorem parallelepiped_eq_convexHull {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module ℝ E] (v : ι → E) : parallelepiped v = (convexHull ℝ) (∑ i : ι, {0, v i})

A parallelepiped is the convex hull of its vertices

theorem parallelepiped_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) : (parallelepiped fun (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 ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) : TopologicalSpace.PositiveCompacts E

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

Equations

• b.parallelepiped = { carrier := parallelepiped ⇑b, isCompact' := ⋯, interior_nonempty' := ⋯ }

@[simp]

theorem Basis.coe_parallelepiped {ι : Type u_1} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ 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 ι'] [NormedAddCommGroup E] [NormedSpace ℝ 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 ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (b : Basis ι ℝ E) (e : E ≃ₗ[ℝ] F) : (b.map e).parallelepiped = TopologicalSpace.PositiveCompacts.map ⇑e ⋯ ⋯ b.parallelepiped

theorem Basis.prod_parallelepiped {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} {F : Type u_4} [Fintype ι] [Fintype ι'] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (v : Basis ι ℝ E) (w : Basis ι' ℝ F) : (v.prod w).parallelepiped = v.parallelepiped.prod w.parallelepiped

theorem Basis.addHaar_def {ι : Type u_5} {E : Type u_6} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) : b.addHaar = MeasureTheory.Measure.addHaarMeasure b.parallelepiped

@[irreducible]

def Basis.addHaar {ι : Type u_5} {E : Type u_6} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) : MeasureTheory.Measure E

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

Equations

• b.addHaar = MeasureTheory.Measure.addHaarMeasure b.parallelepiped

instance IsAddHaarMeasure_basis_addHaar {ι : Type u_1} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) : b.addHaar.IsAddHaarMeasure

instance instSigmaFiniteAddHaar {ι : Type u_1} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) : MeasureTheory.SigmaFinite b.addHaar

theorem Basis.addHaar_eq_iff {ι : Type u_1} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (b : Basis ι ℝ E) (μ : MeasureTheory.Measure E) [MeasureTheory.SigmaFinite μ] [μ.IsAddLeftInvariant] : b.addHaar = μ ↔ μ ↑b.parallelepiped = 1

Let μ be a σ-finite left invariant measure on E. Then μ is equal to the Haar measure defined by b iff the parallelepiped defined by b has measure 1 for μ.

@[simp]

theorem Basis.addHaar_reindex {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) (e : ι ≃ ι') : (b.reindex e).addHaar = b.addHaar

theorem Basis.addHaar_self {ι : Type u_1} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι ℝ E) : b.addHaar (parallelepiped ⇑b) = 1

theorem Basis.prod_addHaar {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} {F : Type u_4} [Fintype ι] [Fintype ι'] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopologyEither E F] (v : Basis ι ℝ E) (w : Basis ι' ℝ F) : (v.prod w).addHaar = v.addHaar.prod w.addHaar

@[instance 100]

instance measureSpaceOfInnerProductSpace {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.MeasureSpace 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 orthonormalBasis.volume_parallelepiped.

This instance creates:

• a potential non-defeq diamond with the natural instance for MeasureSpace (ULift E), which does not exist in Mathlib at the moment;

• a diamond with the existing instance MeasureTheory.Measure.instMeasureSpacePUnit.

However, we've decided not to refactor until one of these diamonds starts creating issues, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Hausdorff.20measure.20normalisation

Equations

• measureSpaceOfInnerProductSpace = MeasureTheory.MeasureSpace.mk (stdOrthonormalBasis ℝ E).toBasis.addHaar

instance instIsAddHaarMeasureVolume {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.volume.IsAddHaarMeasure

instance Real.measureSpace : MeasureTheory.MeasureSpace ℝ

Equations

• Real.measureSpace = inferInstance

Miscellaneous instances for EuclideanSpace

In combination with measureSpaceOfInnerProductSpace, these put a MeasureSpace structure on EuclideanSpace.

instance EuclideanSpace.instMeasurableSpaceReal (ι : Type u_1) : MeasurableSpace (EuclideanSpace ℝ ι)

Equations

• EuclideanSpace.instMeasurableSpaceReal ι = MeasurableSpace.pi

instance EuclideanSpace.instBorelSpaceRealOfFinite (ι : Type u_1) [Finite ι] : BorelSpace (EuclideanSpace ℝ ι)

def EuclideanSpace.measurableEquiv (ι : Type u_1) : EuclideanSpace ℝ ι ≃ᵐ (ι → ℝ)

WithLp.equiv as a MeasurableEquiv.

Equations

• EuclideanSpace.measurableEquiv ι = { toEquiv := WithLp.equiv 2 ((i : ι) → (fun (x : ι) => ℝ) i), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem EuclideanSpace.measurableEquiv_toEquiv (ι : Type u_1) : (EuclideanSpace.measurableEquiv ι).toEquiv = WithLp.equiv 2 ((i : ι) → (fun (x : ι) => ℝ) i)

theorem EuclideanSpace.coe_measurableEquiv (ι : Type u_1) : ⇑(EuclideanSpace.measurableEquiv ι) = ⇑(WithLp.equiv 2 ((i : ι) → (fun (x : ι) => ℝ) i))

theorem EuclideanSpace.coe_measurableEquiv_symm (ι : Type u_1) : ⇑(EuclideanSpace.measurableEquiv ι).symm = ⇑(WithLp.equiv 2 (ι → ℝ)).symm