Lebesgue measure on the real line and on ℝⁿ
#
We show that the Lebesgue measure on the real line (constructed as a particular case of additive
Haar measure on inner product spaces) coincides with the Stieltjes measure associated
to the function x ↦ x
. We deduce properties of this measure on ℝ
, and then of the product
Lebesgue measure on ℝⁿ
. In particular, we prove that they are translation invariant.
We show that, on ℝⁿ
, a linear map acts on Lebesgue measure by rescaling it through the absolute
value of its determinant, in Real.map_linearMap_volume_pi_eq_smul_volume_pi
.
More properties of the Lebesgue measure are deduced from this in
Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
, where they are proved more generally for any
additive Haar measure on a finite-dimensional real vector space.
Definition of the Lebesgue measure and lengths of intervals #
The volume on the real line (as a particular case of the volume on a finite-dimensional inner product space) coincides with the Stieltjes measure coming from the identity function.
Volume of a box in ℝⁿ
#
Images of the Lebesgue measure under multiplication in ℝ #
Images of the Lebesgue measure under translation/linear maps in ℝⁿ #
A diagonal matrix rescales Lebesgue according to its determinant. This is a special case of
Real.map_matrix_volume_pi_eq_smul_volume_pi
, that one should use instead (and whose proof
uses this particular case).
A transvection preserves Lebesgue measure.
Any invertible matrix rescales Lebesgue measure through the absolute value of its determinant.
Any invertible linear map rescales Lebesgue measure through the absolute value of its determinant.
The region between two measurable functions on a measurable set is measurable.
The region between two measurable functions on a measurable set is measurable; a version for the region together with the graph of the upper function.
The region between two measurable functions on a measurable set is measurable; a version for the region together with the graph of the lower function.
The region between two measurable functions on a measurable set is measurable; a version for the region together with the graphs of both functions.
The graph of a measurable function is a measurable set.
The volume of the region between two almost everywhere measurable functions on a measurable set can be represented as a Lebesgue integral.
The region between two a.e.-measurable functions on a null-measurable set is null-measurable.
The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for the region together with the graph of the upper function.
The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for the region together with the graph of the lower function.
The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for the region together with the graphs of both functions.
Consider a real set s
. If a property is true almost everywhere in s ∩ (a, b)
for
all a, b ∈ s
, then it is true almost everywhere in s
. Formulated with μ.restrict
.
See also ae_of_mem_of_ae_of_mem_inter_Ioo
.
Consider a real set s
. If a property is true almost everywhere in s ∩ (a, b)
for
all a, b ∈ s
, then it is true almost everywhere in s
. Formulated with bare membership.
See also ae_restrict_of_ae_restrict_inter_Ioo
.