mathlib3 documentation

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:

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

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

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

Strict subspaces have zero measure #

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.

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

A strict vector 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]

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]

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]

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]

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

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 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.

The Lebesgue measure associated to an alternating map #

@[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 alternating_map.measure

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_aux2 {E : Type u_1} [normed_add_comm_group E] [normed_space E] [measurable_space E] [borel_space E] [finite_dimensional E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (s : set E) (x : E) (h : filter.tendsto (λ (r : ), μ (s metric.closed_ball x r) / μ (metric.closed_ball x r)) (nhds_within 0 (set.Ioi 0)) (nhds 0)) (t u : set E) (h'u : μ u 0) (R : ) (Rpos : 0 < R) (t_bound : t metric.closed_ball 0 R) :
filter.tendsto (λ (r : ), μ (s ({x} + r t)) / μ ({x} + r u)) (nhds_within 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 measure_theory.measure.tendsto_add_haar_inter_smul_one_of_density_one_aux {E : Type u_1} [normed_add_comm_group E] [normed_space E] [measurable_space E] [borel_space E] [finite_dimensional E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (s : set E) (hs : measurable_set s) (x : E) (h : filter.tendsto (λ (r : ), μ (s metric.closed_ball x r) / μ (metric.closed_ball x r)) (nhds_within 0 (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)) (nhds_within 0 (set.Ioi 0)) (nhds 1)
theorem measure_theory.measure.tendsto_add_haar_inter_smul_one_of_density_one {E : Type u_1} [normed_add_comm_group E] [normed_space E] [measurable_space E] [borel_space E] [finite_dimensional E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (s : set E) (x : E) (h : filter.tendsto (λ (r : ), μ (s metric.closed_ball x r) / μ (metric.closed_ball x r)) (nhds_within 0 (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)) (nhds_within 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.

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.