Documentation

Mathlib.MeasureTheory.Measure.Haar.OfBasis

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

The closed parallelepiped spanned by a finite family of vectors.

Equations
Instances For
    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 = Finset.sum Finset.univ fun (i : ι) => t i v i
    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) :
    @[simp]
    theorem parallelepiped_comp_equiv {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [Fintype ι] [Fintype ι'] [AddCommGroup E] [Module E] (v : ιE) (e : ι' ι) :

    Reindexing a family of vectors does not change their parallelepiped.

    theorem parallelepiped_eq_sum_segment {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module E] (v : ιE) :
    parallelepiped v = Finset.sum Finset.univ fun (i : ι) => segment 0 (v i)
    theorem convex_parallelepiped {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module E] (v : ιE) :
    theorem parallelepiped_eq_convexHull {ι : Type u_1} {E : Type u_3} [Fintype ι] [AddCommGroup E] [Module E] (v : ιE) :
    parallelepiped v = (convexHull ) (Finset.sum Finset.univ fun (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.

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

    Equations
    Instances For
      @[simp]
      theorem Basis.coe_parallelepiped {ι : Type u_1} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace E] (b : Basis ι E) :
      @[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 : ι ι') :
      @[irreducible]

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

      Equations
      Instances For

        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 : ι ι') :
        theorem Basis.addHaar_self {ι : Type u_1} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] (b : Basis ι E) :
        (Basis.addHaar b) (parallelepiped b) = 1

        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.

        Equations

        Miscellaneous instances for EuclideanSpace #

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

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

        WithLp.equiv as a MeasurableEquiv.

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