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

• map_linearMap_addHaar_eq_smul_addHaar: a linear map rescales the Haar measure by the absolute value of its determinant.
• addHaar_preimage_linearMap : when f is a linear map with nonzero determinant, the measure of f ⁻¹' s is the measure of s multiplied by the absolute value of the inverse of the determinant of f.
• addHaar_image_linearMap : when f is a linear map, the measure of f '' s is the measure of s multiplied by the absolute value of the determinant of f.
• addHaar_submodule : a strict submodule has measure 0.
• addHaar_smul : the measure of r • s is |r| ^ dim * μ s.
• addHaar_ball: the measure of ball x r is r ^ dim * μ (ball 0 1).
• addHaar_closedBall: the measure of closedBall x r is r ^ dim * μ (ball 0 1).
• addHaar_sphere: spheres have zero measure.

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
• = { carrier := Set.univ.pi fun (x : ι) => Set.Icc 0 1, isCompact' := , interior_nonempty' := }
Instances For
theorem Basis.parallelepiped_basisFun (ι : Type u_1) [] :
(Pi.basisFun ι).parallelepiped =

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

theorem Basis.parallelepiped_eq_map {ι : Type u_1} {E : Type u_2} [] [] (b : Basis ι E) :
b.parallelepiped = TopologicalSpace.PositiveCompacts.map b.equivFun.symm

A parallelepiped can be expressed on the standard basis.

theorem Basis.map_addHaar {ι : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] [] [] (b : Basis ι E) (f : E ≃L[] F) :

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

= MeasureTheory.volume

The Haar measure equals the Lebesgue measure on ℝ.

theorem MeasureTheory.addHaarMeasure_eq_volume_pi (ι : Type u_1) [] :
= MeasureTheory.volume

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

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

### Strict subspaces have zero measure #

theorem MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {s : Set E} (u : E) (sb : ) (hu : ) (hs : Pairwise (Disjoint on fun (n : ) => {u n} + s)) (h'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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {s : Set E} (u : E) (hu : ) (hs : Pairwise (Disjoint on fun (n : ) => {u n} + s)) (h'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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : ) (hs : s ) :
μ s = 0

A strict vector subspace has measure zero.

theorem MeasureTheory.Measure.addHaar_affineSubspace {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : ) (hs : s ) :
μ s = 0

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} [] {f : (ι) →ₗ[] ι} (hf : LinearMap.det f 0) (μ : MeasureTheory.Measure (ι)) [μ.IsAddHaarMeasure] :
= ENNReal.ofReal |(LinearMap.det f)⁻¹| μ
theorem MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {f : E →ₗ[] E} (hf : LinearMap.det f 0) :
= ENNReal.ofReal |(LinearMap.det f)⁻¹| μ
@[simp]
theorem MeasureTheory.Measure.addHaar_preimage_linearMap {E : Type u_1} [] [] [] [] (μ : ) [μ.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} [] [] [] [] (μ : ) [μ.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} [] [] [] [] (μ : ) [μ.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} [] [] [] [] (μ : ) [μ.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} [] [] [] [] (μ : ) [μ.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} [] [] [] [] (μ : ) [μ.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} [] [] [] [] (μ : ) [μ.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.

theorem MeasureTheory.Measure.LinearMap.quasiMeasurePreserving {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (f : E →ₗ[] E) (hf : LinearMap.det f 0) :
theorem MeasureTheory.Measure.ContinuousLinearMap.quasiMeasurePreserving {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (f : E →L[] E) (hf : f.det 0) :

### Basic properties of Haar measures on real vector spaces #

theorem MeasureTheory.Measure.map_addHaar_smul {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {r : } (hr : r 0) :
MeasureTheory.Measure.map (fun (x : E) => r x) μ = μ
theorem MeasureTheory.Measure.quasiMeasurePreserving_smul {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {r : } (hr : r 0) :
@[simp]
theorem MeasureTheory.Measure.addHaar_preimage_smul {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {r : } (hr : r 0) (s : Set E) :
μ ((fun (x : E) => r x) ⁻¹' s) = * μ s
@[simp]
theorem MeasureTheory.Measure.addHaar_smul {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (r : ) (s : Set E) :
μ (r s) = * μ 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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {r : } (hr : 0 r) (s : Set E) :
μ (r s) = * μ s
theorem MeasureTheory.Measure.NullMeasurableSet.const_smul {E : Type u_1} [] [] [] [] {μ : } [μ.IsAddHaarMeasure] {s : Set E} (hs : ) (r : ) :
@[simp]
theorem MeasureTheory.Measure.addHaar_image_homothety {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) (r : ) (s : Set E) :
μ ( '' s) = * μ s

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} [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) (r : ) :
μ (Metric.ball x r) = μ (Metric.ball 0 r)
theorem MeasureTheory.Measure.addHaar_closedBall_center {E : Type u_3} [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) (r : ) :
μ = μ
theorem MeasureTheory.Measure.addHaar_ball_mul_of_pos {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 < r) (s : ) :
μ (Metric.ball x (r * s)) = * μ (Metric.ball 0 s)
theorem MeasureTheory.Measure.addHaar_ball_of_pos {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 < r) :
μ (Metric.ball x r) = * μ (Metric.ball 0 1)
theorem MeasureTheory.Measure.addHaar_ball_mul {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] [] (x : E) {r : } (hr : 0 r) (s : ) :
μ (Metric.ball x (r * s)) = * μ (Metric.ball 0 s)
theorem MeasureTheory.Measure.addHaar_ball {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] [] (x : E) {r : } (hr : 0 r) :
μ (Metric.ball x r) = * μ (Metric.ball 0 1)
theorem MeasureTheory.Measure.addHaar_closedBall_mul_of_pos {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 < r) (s : ) :
μ (Metric.closedBall x (r * s)) = * μ
theorem MeasureTheory.Measure.addHaar_closedBall_mul {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 r) {s : } (hs : 0 s) :
μ (Metric.closedBall x (r * s)) = * μ
theorem MeasureTheory.Measure.addHaar_closedBall' {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 r) :
μ = * μ

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_closed_unit_ball_eq_addHaar_unit_ball {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] :
μ = μ (Metric.ball 0 1)
theorem MeasureTheory.Measure.addHaar_closedBall {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : 0 r) :
μ = * μ (Metric.ball 0 1)
theorem MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] [] (x : E) (r : ) :
μ = μ (Metric.ball x r)
theorem MeasureTheory.Measure.addHaar_sphere_of_ne_zero {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (x : E) {r : } (hr : r 0) :
μ (Metric.sphere x r) = 0
theorem MeasureTheory.Measure.addHaar_sphere {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] [] (x : E) (r : ) :
μ (Metric.sphere x r) = 0
theorem MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_smul {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] {r : } (hr : r 0) (x : E) (y : E) (s : Set E) (t : Set E) :
μ ({x} + r s) / μ ({y} + r t) = μ s / μ t
@[instance 100]
instance MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure {E : Type u_1} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] :
Equations
• =

### The Lebesgue measure associated to an alternating map #

theorem MeasureTheory.Measure.addHaar_parallelepiped {ι : Type u_3} {G : Type u_4} [] [] [] [] [] (b : Basis ι G) (v : ιG) :
b.addHaar = ENNReal.ofReal |b.det v|
theorem AlternatingMap.measure_def {G : Type u_5} [] [] [] [] {n : } [_i : Fact ] (ω : ) :
@[irreducible]
noncomputable def AlternatingMap.measure {G : Type u_5} [] [] [] [] {n : } [_i : Fact ] (ω : ) :

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
theorem AlternatingMap.measure_parallelepiped {G : Type u_4} [] [] [] [] {n : } [_i : Fact ] (ω : ) (v : Fin nG) :
ω.measure = ENNReal.ofReal |ω v|
instance MeasureTheory.Measure.instIsAddLeftInvariantMeasure {G : Type u_4} [] [] [] [] {n : } [_i : Fact ] (ω : ) :
Equations
• =
instance MeasureTheory.Measure.instIsLocallyFiniteMeasureMeasure {G : Type u_4} [] [] [] [] {n : } [_i : Fact ] (ω : ) :
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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s ) / μ ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t : Set E) (u : Set E) (h'u : μ u 0) (t_bound : t ) :
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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s ) / μ ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t : Set E) (u : Set E) (h'u : μ u 0) (R : ) (Rpos : 0 < R) (t_bound : t ) :
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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s ) / μ ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (t : Set E) (ht : ) (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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : Set E) (hs : ) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s ) / μ ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : ) (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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s ) / μ ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : ) (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} [] [] [] [] (μ : ) [μ.IsAddHaarMeasure] (s : Set E) (x : E) (h : Filter.Tendsto (fun (r : ) => μ (s ) / μ ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)) (t : Set E) (ht : ) (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.