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: whenfis a linear map with nonzero determinant, the measure off ⁻¹' sis the measure ofsmultiplied by the absolute value of the inverse of the determinant off.addHaar_image_linearMap: whenfis a linear map, the measure off '' sis the measure ofsmultiplied by the absolute value of the determinant off.addHaar_submodule: a strict submodule has measure0.addHaar_smul: the measure ofr • sis|r| ^ dim * μ s.addHaar_ball: the measure ofball x risr ^ dim * μ (ball 0 1).addHaar_closedBall: the measure ofclosedBall x risr ^ 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
- TopologicalSpace.PositiveCompacts.piIcc01 ι = { carrier := Set.univ.pi fun (x : ι) => Set.Icc 0 1, isCompact' := ⋯, interior_nonempty' := ⋯ }
Instances For
The parallelepiped formed from the standard basis for ι → ℝ is [0,1]^ι
A parallelepiped can be expressed on the standard basis.
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 ℝ^ι.
Equations
- ⋯ = ⋯
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.
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.
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.
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.
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.
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.
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.
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.
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 #
Rescaling a set by a factor r multiplies its measure by abs (r ^ dim).
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 #
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.
Equations
- ⋯ = ⋯
The Lebesgue measure associated to an alternating map #
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.
Instances For
Equations
- ⋯ = ⋯
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
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.
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.