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 Lebesgue measure is a Haar measure on ℝ and on ℝ^ι. #

Strict subspaces have zero measure #

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.

Basic properties of Haar measures on real vector spaces #

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 #

The Lebesgue measure associated to an alternating map #

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