mathlib3documentation

measure_theory.measure.lebesgue.eq_haar

Relationship between the Haar and Lebesgue measures #

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

We prove that the Haar measure and Lebesgue measure are equal on ℝ and on ℝ^ι, in measure_theory.add_haar_measure_eq_volume and measure_theory.add_haar_measure_eq_volume_pi.

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

• map_linear_map_add_haar_eq_smul_add_haar: a linear map rescales the Haar measure by the absolute value of its determinant.
• add_haar_preimage_linear_map : 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.
• add_haar_image_linear_map : 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.
• add_haar_submodule : a strict submodule has measure 0.
• add_haar_smul : the measure of r • s is |r| ^ dim * μ s.
• add_haar_ball: the measure of ball x r is r ^ dim * μ (ball 0 1).
• add_haar_closed_ball: the measure of closed_ball x r is r ^ dim * μ (ball 0 1).
• add_haar_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 alternating_map.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_add_haar_inter_smul_one_of_density_one. In particular, s intersects {x} + r • t for small r, see eventually_nonempty_inter_smul_of_density_one.

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

Equations

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

Equations
theorem basis.parallelepiped_basis_fun (ι : Type u_1) [fintype ι] :

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

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 ℝ^ι.

@[protected, instance]

Strict subspaces have zero measure #

theorem measure_theory.measure.add_haar_eq_zero_of_disjoint_translates_aux {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {s : set E} (u : E) (sb : metric.bounded s) (hu : metric.bounded (set.range u)) (hs : pairwise (disjoint on λ (n : ), {u n} + s)) (h's : measurable_set 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 measure_theory.measure.add_haar_eq_zero_of_disjoint_translates {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {s : set E} (u : E) (hu : metric.bounded (set.range u)) (hs : pairwise (disjoint on λ (n : ), {u n} + s)) (h's : measurable_set s) :
μ s = 0

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

theorem measure_theory.measure.add_haar_submodule {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : E) (hs : s ) :
μ s = 0

A strict vector subspace has measure zero.

theorem measure_theory.measure.add_haar_affine_subspace {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : E) (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.

@[simp]
theorem measure_theory.measure.add_haar_preimage_linear_map {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {f : E →ₗ[] E} (hf : 0) (s : set E) :
μ (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 measure_theory.measure.add_haar_preimage_continuous_linear_map {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {f : E →L[] E} (hf : 0) (s : set E) :
μ (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]

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]

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 measure_theory.measure.add_haar_image_linear_map {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (f : E →ₗ[] E) (s : set E) :
μ (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]

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]

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 measure_theory.measure.add_haar_preimage_smul {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {r : } (hr : r 0) (s : set E) :
@[simp]
theorem measure_theory.measure.add_haar_smul {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (r : ) (s : set E) :
μ (r s) = * μ s

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

theorem measure_theory.measure.add_haar_smul_of_nonneg {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {r : } (hr : 0 r) (s : set E) :
μ (r s) = ennreal.of_real (r ^ fdim E) * μ s
theorem measure_theory.measure.null_measurable_set.const_smul {E : Type u_1} [ E] [borel_space E] {μ : measure_theory.measure E} {s : set E} (hs : μ) (r : ) :
@[simp]
theorem measure_theory.measure.add_haar_image_homothety {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) (r : ) (s : set E) :
μ ( r) '' s) = * μ s

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

Measure of balls #

theorem measure_theory.measure.add_haar_ball_center {E : Type u_1} [borel_space E] (μ : measure_theory.measure E) (x : E) (r : ) :
μ r) = μ r)
theorem measure_theory.measure.add_haar_ball_mul_of_pos {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 < r) (s : ) :
μ (r * s)) = ennreal.of_real (r ^ fdim E) * μ s)
theorem measure_theory.measure.add_haar_ball_of_pos {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 < r) :
μ r) = ennreal.of_real (r ^ fdim E) * μ 1)
theorem measure_theory.measure.add_haar_ball_mul {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) [nontrivial E] (x : E) {r : } (hr : 0 r) (s : ) :
μ (r * s)) = ennreal.of_real (r ^ fdim E) * μ s)
theorem measure_theory.measure.add_haar_ball {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) [nontrivial E] (x : E) {r : } (hr : 0 r) :
μ r) = ennreal.of_real (r ^ fdim E) * μ 1)
theorem measure_theory.measure.add_haar_closed_ball_mul_of_pos {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 < r) (s : ) :
μ (r * s)) = ennreal.of_real (r ^ fdim E) * μ s)
theorem measure_theory.measure.add_haar_closed_ball_mul {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 r) {s : } (hs : 0 s) :
μ (r * s)) = ennreal.of_real (r ^ fdim E) * μ s)
theorem measure_theory.measure.add_haar_closed_ball' {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 r) :
μ r) = ennreal.of_real (r ^ fdim E) * μ 1)

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

theorem measure_theory.measure.add_haar_closed_ball {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 r) :
μ r) = ennreal.of_real (r ^ fdim E) * μ 1)
theorem measure_theory.measure.add_haar_sphere_of_ne_zero {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : r 0) :
μ r) = 0
theorem measure_theory.measure.add_haar_sphere {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) [nontrivial E] (x : E) (r : ) :
μ r) = 0
theorem measure_theory.measure.add_haar_singleton_add_smul_div_singleton_add_smul {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) {r : } (hr : r 0) (x y : E) (s t : set E) :
μ ({x} + r s) / μ ({y} + r t) = μ s / μ t
@[protected, instance]
Equations

The Lebesgue measure associated to an alternating map #

theorem measure_theory.measure.add_haar_parallelepiped {ι : Type u_3} {G : Type u_4} [fintype ι] [decidable_eq ι] [ G] [borel_space G] (b : G) (v : ι G) :
@[irreducible]
noncomputable def alternating_map.measure {G : Type u_4} [ G] [borel_space G] {n : } [fact (fdim G = n)] (ω : (fin n)) :

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 alternating_map.measure
theorem alternating_map.measure_parallelepiped {G : Type u_4} [ G] [borel_space G] {n : } [fact (fdim G = n)] (ω : (fin n)) (v : fin n G) :
@[protected, instance]
@[protected, instance]

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 ∩ closed_ball x r) / μ (closed_ball 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_add_haar_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_add_haar_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_add_haar_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_add_haar_inter_smul_one_of_density_one_aux, and then without this assumption in tendsto_add_haar_inter_smul_one_of_density_one by applying the previous lemma to the measurable hull to_measurable μ s

theorem measure_theory.measure.tendsto_add_haar_inter_smul_zero_of_density_zero_aux1 {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : set E) (x : E) (h : filter.tendsto (λ (r : ), μ (s / μ r)) (set.Ioi 0)) (nhds 0)) (t u : set E) (h'u : μ u 0) (t_bound : t ) :
filter.tendsto (λ (r : ), μ (s ({x} + r t)) / μ ({x} + r u)) (set.Ioi 0)) (nhds 0)
theorem measure_theory.measure.tendsto_add_haar_inter_smul_zero_of_density_zero_aux2 {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : set E) (x : E) (h : filter.tendsto (λ (r : ), μ (s / μ r)) (set.Ioi 0)) (nhds 0)) (t u : set E) (h'u : μ u 0) (R : ) (Rpos : 0 < R) (t_bound : t ) :
filter.tendsto (λ (r : ), μ (s ({x} + r t)) / μ ({x} + r u)) (set.Ioi 0)) (nhds 0)
theorem measure_theory.measure.tendsto_add_haar_inter_smul_zero_of_density_zero {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : set E) (x : E) (h : filter.tendsto (λ (r : ), μ (s / μ r)) (set.Ioi 0)) (nhds 0)) (t : set E) (ht : measurable_set t) (h''t : μ t ) :
filter.tendsto (λ (r : ), μ (s ({x} + r t)) / μ ({x} + r t)) (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 measure_theory.measure.tendsto_add_haar_inter_smul_one_of_density_one_aux {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : set E) (hs : measurable_set s) (x : E) (h : filter.tendsto (λ (r : ), μ (s / μ r)) (set.Ioi 0)) (nhds 1)) (t : set E) (ht : measurable_set t) (h't : μ t 0) (h''t : μ t ) :
filter.tendsto (λ (r : ), μ (s ({x} + r t)) / μ ({x} + r t)) (set.Ioi 0)) (nhds 1)
theorem measure_theory.measure.tendsto_add_haar_inter_smul_one_of_density_one {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : set E) (x : E) (h : filter.tendsto (λ (r : ), μ (s / μ r)) (set.Ioi 0)) (nhds 1)) (t : set E) (ht : measurable_set t) (h't : μ t 0) (h''t : μ t ) :
filter.tendsto (λ (r : ), μ (s ({x} + r t)) / μ ({x} + r t)) (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 measure_theory.measure.eventually_nonempty_inter_smul_of_density_one {E : Type u_1} [ E] [borel_space E] (μ : measure_theory.measure E) (s : set E) (x : E) (h : filter.tendsto (λ (r : ), μ (s / μ r)) (set.Ioi 0)) (nhds 1)) (t : set E) (ht : measurable_set t) (h't : μ t 0) :
∀ᶠ (r : ) in (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.