Documentation

Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Relationship between the Haar and Lebesgue measures #

We prove that the Haar measure and Lebesgue measure are equal on and on ℝ^ι, in MeasureTheory.addHaarMeasure_eq_volume and MeasureTheory.addHaarMeasure_eq_volume_pi.

We deduce basic properties of any Haar measure on a finite dimensional real vector space:

This makes it possible to associate a Lebesgue measure to an n-alternating map in dimension n. This measure is called AlternatingMap.measure. Its main property is ω.measure_parallelepiped v, stating that the associated measure of the parallelepiped spanned by vectors v₁, ..., vₙ is given by |ω v|.

We also show that a Lebesgue density point x of a set s (with respect to closed balls) has density one for the rescaled copies {x} + r • t of a given set t with positive measure, in tendsto_addHaar_inter_smul_one_of_density_one. In particular, s intersects {x} + r • t for small r, see eventually_nonempty_inter_smul_of_density_one.

Statements on integrals of functions with respect to an additive Haar measure can be found in MeasureTheory.Measure.Haar.NormedSpace.

The interval [0,1] as a compact set with non-empty interior.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The set [0,1]^ι as a compact set with non-empty interior.

    Equations
    Instances For

      The parallelepiped formed from the standard basis for ι → ℝ is [0,1]^ι

      theorem Basis.parallelepiped_eq_map {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [NormedSpace E] (b : Basis ι E) :

      A parallelepiped can be expressed on the standard basis.

      theorem Basis.map_addHaar {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace E] [NormedSpace F] [MeasurableSpace E] [MeasurableSpace F] [BorelSpace E] [BorelSpace F] [SecondCountableTopology F] [SigmaCompactSpace F] (b : Basis ι E) (f : E ≃L[] F) :
      MeasureTheory.Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar

      The Lebesgue measure is a Haar measure on and on ℝ^ι. #

      The Haar measure equals the Lebesgue measure on .

      The Haar measure equals the Lebesgue measure on ℝ^ι.

      instance MeasureTheory.isAddHaarMeasure_volume_pi (ι : Type u_1) [Fintype ι] :
      MeasureTheory.volume.IsAddHaarMeasure
      Equations
      • =

      Strict subspaces have zero measure #

      theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (u : E) (sb : Bornology.IsBounded s) (hu : Bornology.IsBounded (Set.range u)) (hs : Pairwise (Disjoint on fun (n : ) => {u n} + s)) (h's : MeasurableSet s) :
      μ s = 0

      If a set is disjoint of its translates by infinitely many bounded vectors, then it has measure zero. This auxiliary lemma proves this assuming additionally that the set is bounded.

      theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (u : E) (hu : Bornology.IsBounded (Set.range u)) (hs : Pairwise (Disjoint on fun (n : ) => {u n} + s)) (h's : MeasurableSet s) :
      μ s = 0

      If a set is disjoint of its translates by infinitely many bounded vectors, then it has measure zero.

      theorem MeasureTheory.Measure.addHaar_submodule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Submodule E) (hs : s ) :
      μ s = 0

      A strict vector subspace has measure zero.

      A strict affine subspace has measure zero.

      Applying a linear map rescales Haar measure by the determinant #

      We first prove this on ι → ℝ, using that this is already known for the product Lebesgue measure (thanks to matrices computations). Then, we extend this to any finite-dimensional real vector space by using a linear equiv with a space of the form ι → ℝ, and arguing that such a linear equiv maps Haar measure to Haar measure.

      theorem MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar {ι : Type u_1} [Finite ι] {f : (ι) →ₗ[] ι} (hf : LinearMap.det f 0) (μ : MeasureTheory.Measure (ι)) [μ.IsAddHaarMeasure] :
      MeasureTheory.Measure.map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| μ
      theorem MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E →ₗ[] E} (hf : LinearMap.det f 0) :
      MeasureTheory.Measure.map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| μ
      @[simp]
      theorem MeasureTheory.Measure.addHaar_preimage_linearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E →ₗ[] E} (hf : LinearMap.det f 0) (s : Set E) :
      μ (f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s

      The preimage of a set s under a linear map f with nonzero determinant has measure equal to μ s times the absolute value of the inverse of the determinant of f.

      @[simp]
      theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E →L[] E} (hf : LinearMap.det f 0) (s : Set E) :
      μ (f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s

      The preimage of a set s under a continuous linear map f with nonzero determinant has measure equal to μ s times the absolute value of the inverse of the determinant of f.

      @[simp]
      theorem MeasureTheory.Measure.addHaar_preimage_linearEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E ≃ₗ[] E) (s : Set E) :
      μ (f ⁻¹' s) = ENNReal.ofReal |LinearMap.det f.symm| * μ s

      The preimage of a set s under a linear equiv f has measure equal to μ s times the absolute value of the inverse of the determinant of f.

      @[simp]
      theorem MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E ≃L[] E) (s : Set E) :
      μ (f ⁻¹' s) = ENNReal.ofReal |LinearMap.det f.symm| * μ s

      The preimage of a set s under a continuous linear equiv f has measure equal to μ s times the absolute value of the inverse of the determinant of f.

      @[simp]
      theorem MeasureTheory.Measure.addHaar_image_linearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E →ₗ[] E) (s : Set E) :
      μ (f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s

      The image of a set s under a linear map f has measure equal to μ s times the absolute value of the determinant of f.

      @[simp]
      theorem MeasureTheory.Measure.addHaar_image_continuousLinearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E →L[] E) (s : Set E) :
      μ (f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s

      The image of a set s under a continuous linear map f has measure equal to μ s times the absolute value of the determinant of f.

      @[simp]
      theorem MeasureTheory.Measure.addHaar_image_continuousLinearEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E ≃L[] E) (s : Set E) :
      μ (f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s

      The image of a set s under a continuous linear equiv f has measure equal to μ s times the absolute value of the determinant of f.

      Basic properties of Haar measures on real vector spaces #

      @[simp]
      theorem MeasureTheory.Measure.addHaar_preimage_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : } (hr : r 0) (s : Set E) :
      μ ((fun (x : E) => r x) ⁻¹' s) = ENNReal.ofReal |(r ^ Module.finrank E)⁻¹| * μ s
      @[simp]
      theorem MeasureTheory.Measure.addHaar_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (r : ) (s : Set E) :
      μ (r s) = ENNReal.ofReal |r ^ Module.finrank E| * μ s

      Rescaling a set by a factor r multiplies its measure by abs (r ^ dim).

      theorem MeasureTheory.Measure.addHaar_smul_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : } (hr : 0 r) (s : Set E) :
      μ (r s) = ENNReal.ofReal (r ^ Module.finrank E) * μ s
      @[simp]

      We don't need to state map_addHaar_neg here, because it has already been proved for general Haar measures on general commutative groups.

      Measure of balls #

      theorem MeasureTheory.Measure.addHaar_ball_center {E : Type u_3} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ) :
      μ (Metric.ball x r) = μ (Metric.ball 0 r)
      theorem MeasureTheory.Measure.addHaar_ball_mul_of_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 < r) (s : ) :
      theorem MeasureTheory.Measure.addHaar_ball_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) {r : } (hr : 0 r) (s : ) :
      theorem MeasureTheory.Measure.addHaar_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) {r : } (hr : 0 r) :
      theorem MeasureTheory.Measure.addHaar_closedBall_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 r) {s : } (hs : 0 s) :

      The measure of a closed ball can be expressed in terms of the measure of the closed unit ball. Use instead addHaar_closedBall, which uses the measure of the open unit ball as a standard form.

      theorem MeasureTheory.Measure.addHaar_sphere_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : r 0) :
      μ (Metric.sphere x r) = 0
      theorem MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : } (hr : r 0) (x : E) (y : E) (s : Set E) (t : Set E) :
      μ ({x} + r s) / μ ({y} + r t) = μ s / μ t

      The Lebesgue measure associated to an alternating map #

      theorem MeasureTheory.Measure.addHaar_parallelepiped {ι : Type u_3} {G : Type u_4} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup G] [NormedSpace G] [MeasurableSpace G] [BorelSpace G] (b : Basis ι G) (v : ιG) :
      b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|
      @[irreducible]

      The Lebesgue measure associated to an alternating map. It gives measure |ω v| to the parallelepiped spanned by the vectors v₁, ..., vₙ. Note that it is not always a Haar measure, as it can be zero, but it is always locally finite and translation invariant.

      Equations
      Instances For
        Equations
        • =

        Density points #

        Besicovitch covering theorem ensures that, for any locally finite measure on a finite-dimensional real vector space, almost every point of a set s is a density point, i.e., μ (s ∩ closedBall x r) / μ (closedBall x r) tends to 1 as r tends to 0 (see Besicovitch.ae_tendsto_measure_inter_div). When μ is a Haar measure, one can deduce the same property for any rescaling sequence of sets, of the form {x} + r • t where t is a set with positive finite measure, instead of the sequence of closed balls.

        We argue first for the dual property, i.e., if s has density 0 at x, then μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) tends to 0. First when t is contained in the ball of radius 1, in tendsto_addHaar_inter_smul_zero_of_density_zero_aux1, (by arguing by inclusion). Then when t is bounded, reducing to the previous one by rescaling, in tendsto_addHaar_inter_smul_zero_of_density_zero_aux2. Then for a general set t, by cutting it into a bounded part and a part with small measure, in tendsto_addHaar_inter_smul_zero_of_density_zero. Going to the complement, one obtains the desired property at points of density 1, first when s is measurable in tendsto_addHaar_inter_smul_one_of_density_one_aux, and then without this assumption in tendsto_addHaar_inter_smul_one_of_density_one by applying the previous lemma to the measurable hull toMeasurable μ s

        theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t : Set E) (u : Set E) (h'u : μ u 0) (t_bound : t Metric.closedBall 0 1) :
        Filter.Tendsto (fun (r : ) => μ (s ({x} + r t)) / μ ({x} + r u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
        theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t : Set E) (u : Set E) (h'u : μ u 0) (R : ) (Rpos : 0 < R) (t_bound : t Metric.closedBall 0 R) :
        Filter.Tendsto (fun (r : ) => μ (s ({x} + r t)) / μ ({x} + r u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
        theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t : Set E) (ht : MeasurableSet t) (h''t : μ t ) :
        Filter.Tendsto (fun (r : ) => μ (s ({x} + r t)) / μ ({x} + r t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

        Consider a point x at which a set s has density zero, with respect to closed balls. Then it also has density zero with respect to any measurable set t: the proportion of points in s belonging to a rescaled copy {x} + r • t of t tends to zero as r tends to zero.

        theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (hs : MeasurableSet s) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : MeasurableSet t) (h't : μ t 0) (h''t : μ t ) :
        Filter.Tendsto (fun (r : ) => μ (s ({x} + r t)) / μ ({x} + r t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
        theorem MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : MeasurableSet t) (h't : μ t 0) (h''t : μ t ) :
        Filter.Tendsto (fun (r : ) => μ (s ({x} + r t)) / μ ({x} + r t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

        Consider a point x at which a set s has density one, with respect to closed balls (i.e., a Lebesgue density point of s). Then s has also density one at x with respect to any measurable set t: the proportion of points in s belonging to a rescaled copy {x} + r • t of t tends to one as r tends to zero.

        theorem MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : MeasurableSet t) (h't : μ t 0) :
        ∀ᶠ (r : ) in nhdsWithin 0 (Set.Ioi 0), (s ({x} + r t)).Nonempty

        Consider a point x at which a set s has density one, with respect to closed balls (i.e., a Lebesgue density point of s). Then s intersects the rescaled copies {x} + r • t of a given set t with positive measure, for any small enough r.