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

theorem Real.volume_eq_stieltjes_id :
MeasureTheory.volume = StieltjesFunction.id.measure

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.

theorem Real.volume_val (s : ) :
MeasureTheory.volume s = StieltjesFunction.id.measure s
@[simp]
theorem Real.volume_Ico {a : } {b : } :
MeasureTheory.volume (Set.Ico a b) = ENNReal.ofReal (b - a)
@[simp]
theorem Real.volume_Icc {a : } {b : } :
MeasureTheory.volume (Set.Icc a b) = ENNReal.ofReal (b - a)
@[simp]
theorem Real.volume_Ioo {a : } {b : } :
MeasureTheory.volume (Set.Ioo a b) = ENNReal.ofReal (b - a)
@[simp]
theorem Real.volume_Ioc {a : } {b : } :
MeasureTheory.volume (Set.Ioc a b) = ENNReal.ofReal (b - a)
theorem Real.volume_singleton {a : } :
MeasureTheory.volume {a} = 0
theorem Real.volume_univ :
MeasureTheory.volume Set.univ =
@[simp]
theorem Real.volume_ball (a : ) (r : ) :
MeasureTheory.volume () = ENNReal.ofReal (2 * r)
@[simp]
theorem Real.volume_closedBall (a : ) (r : ) :
MeasureTheory.volume () = ENNReal.ofReal (2 * r)
@[simp]
theorem Real.volume_emetric_ball (a : ) (r : ENNReal) :
MeasureTheory.volume () = 2 * r
@[simp]
theorem Real.volume_emetric_closedBall (a : ) (r : ENNReal) :
MeasureTheory.volume () = 2 * r
instance Real.noAtoms_volume :
MeasureTheory.NoAtoms MeasureTheory.volume
Equations
@[simp]
theorem Real.volume_interval {a : } {b : } :
MeasureTheory.volume (Set.uIcc a b) = ENNReal.ofReal |b - a|
@[simp]
theorem Real.volume_Ioi {a : } :
MeasureTheory.volume () =
@[simp]
theorem Real.volume_Ici {a : } :
MeasureTheory.volume () =
@[simp]
theorem Real.volume_Iio {a : } :
MeasureTheory.volume () =
@[simp]
theorem Real.volume_Iic {a : } :
MeasureTheory.volume () =
instance Real.isFiniteMeasure_restrict_Icc (x : ) (y : ) :
MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Icc x y))
Equations
• =
instance Real.isFiniteMeasure_restrict_Ico (x : ) (y : ) :
MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ico x y))
Equations
• =
instance Real.isFiniteMeasure_restrict_Ioc (x : ) (y : ) :
MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ioc x y))
Equations
• =
instance Real.isFiniteMeasure_restrict_Ioo (x : ) (y : ) :
MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ioo x y))
Equations
• =
theorem Real.volume_le_diam (s : ) :
MeasureTheory.volume s
theorem Filter.Eventually.volume_pos_of_nhds_real {p : } {a : } (h : ∀ᶠ (x : ) in nhds a, p x) :
0 < MeasureTheory.volume {x : | p x}

### Volume of a box in ℝⁿ#

theorem Real.volume_Icc_pi {ι : Type u_1} [] {a : ι} {b : ι} :
MeasureTheory.volume (Set.Icc a b) = Finset.univ.prod fun (i : ι) => ENNReal.ofReal (b i - a i)
@[simp]
theorem Real.volume_Icc_pi_toReal {ι : Type u_1} [] {a : ι} {b : ι} (h : a b) :
(MeasureTheory.volume (Set.Icc a b)).toReal = Finset.univ.prod fun (i : ι) => b i - a i
theorem Real.volume_pi_Ioo {ι : Type u_1} [] {a : ι} {b : ι} :
MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioo (a i) (b i)) = Finset.univ.prod fun (i : ι) => ENNReal.ofReal (b i - a i)
@[simp]
theorem Real.volume_pi_Ioo_toReal {ι : Type u_1} [] {a : ι} {b : ι} (h : a b) :
(MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioo (a i) (b i))).toReal = Finset.univ.prod fun (i : ι) => b i - a i
theorem Real.volume_pi_Ioc {ι : Type u_1} [] {a : ι} {b : ι} :
MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioc (a i) (b i)) = Finset.univ.prod fun (i : ι) => ENNReal.ofReal (b i - a i)
@[simp]
theorem Real.volume_pi_Ioc_toReal {ι : Type u_1} [] {a : ι} {b : ι} (h : a b) :
(MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ioc (a i) (b i))).toReal = Finset.univ.prod fun (i : ι) => b i - a i
theorem Real.volume_pi_Ico {ι : Type u_1} [] {a : ι} {b : ι} :
MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ico (a i) (b i)) = Finset.univ.prod fun (i : ι) => ENNReal.ofReal (b i - a i)
@[simp]
theorem Real.volume_pi_Ico_toReal {ι : Type u_1} [] {a : ι} {b : ι} (h : a b) :
(MeasureTheory.volume (Set.univ.pi fun (i : ι) => Set.Ico (a i) (b i))).toReal = Finset.univ.prod fun (i : ι) => b i - a i
@[simp]
theorem Real.volume_pi_ball {ι : Type u_1} [] (a : ι) {r : } (hr : 0 < r) :
MeasureTheory.volume () = ENNReal.ofReal ((2 * r) ^ )
@[simp]
theorem Real.volume_pi_closedBall {ι : Type u_1} [] (a : ι) {r : } (hr : 0 r) :
MeasureTheory.volume () = ENNReal.ofReal ((2 * r) ^ )
theorem Real.volume_pi_le_prod_diam {ι : Type u_1} [] (s : Set (ι)) :
MeasureTheory.volume s Finset.univ.prod fun (i : ι) => EMetric.diam ()
theorem Real.volume_pi_le_diam_pow {ι : Type u_1} [] (s : Set (ι)) :
MeasureTheory.volume s

### Images of the Lebesgue measure under multiplication in ℝ #

theorem Real.smul_map_volume_mul_left {a : } (h : a 0) :
MeasureTheory.Measure.map (fun (x : ) => a * x) MeasureTheory.volume = MeasureTheory.volume
theorem Real.map_volume_mul_left {a : } (h : a 0) :
MeasureTheory.Measure.map (fun (x : ) => a * x) MeasureTheory.volume = MeasureTheory.volume
@[simp]
theorem Real.volume_preimage_mul_left {a : } (h : a 0) (s : ) :
MeasureTheory.volume ((fun (x : ) => a * x) ⁻¹' s) = * MeasureTheory.volume s
theorem Real.smul_map_volume_mul_right {a : } (h : a 0) :
MeasureTheory.Measure.map (fun (x : ) => x * a) MeasureTheory.volume = MeasureTheory.volume
theorem Real.map_volume_mul_right {a : } (h : a 0) :
MeasureTheory.Measure.map (fun (x : ) => x * a) MeasureTheory.volume = MeasureTheory.volume
@[simp]
theorem Real.volume_preimage_mul_right {a : } (h : a 0) (s : ) :
MeasureTheory.volume ((fun (x : ) => x * a) ⁻¹' s) = * MeasureTheory.volume s

### Images of the Lebesgue measure under translation/linear maps in ℝⁿ #

theorem Real.smul_map_diagonal_volume_pi {ι : Type u_1} [] [] {D : ι} (h : ().det 0) :
ENNReal.ofReal |().det| MeasureTheory.Measure.map ((Matrix.toLin' ())) MeasureTheory.volume = MeasureTheory.volume

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

theorem Real.volume_preserving_transvectionStruct {ι : Type u_1} [] [] (t : ) :
MeasureTheory.MeasurePreserving ((Matrix.toLin' t.toMatrix)) MeasureTheory.volume MeasureTheory.volume

A transvection preserves Lebesgue measure.

theorem Real.map_matrix_volume_pi_eq_smul_volume_pi {ι : Type u_1} [] [] {M : Matrix ι ι } (hM : M.det 0) :
MeasureTheory.Measure.map ((Matrix.toLin' M)) MeasureTheory.volume = ENNReal.ofReal |M.det⁻¹| MeasureTheory.volume

Any invertible matrix rescales Lebesgue measure through the absolute value of its determinant.

theorem Real.map_linearMap_volume_pi_eq_smul_volume_pi {ι : Type u_1} [] {f : (ι) →ₗ[] ι} (hf : LinearMap.det f 0) :
MeasureTheory.Measure.map (f) MeasureTheory.volume = ENNReal.ofReal |(LinearMap.det f)⁻¹| MeasureTheory.volume

Any invertible linear map rescales Lebesgue measure through the absolute value of its determinant.

def regionBetween {α : Type u_1} (f : α) (g : α) (s : Set α) :
Set (α × )

The region between two real-valued functions on an arbitrary set.

Equations
Instances For
theorem regionBetween_subset {α : Type u_1} (f : α) (g : α) (s : Set α) :
s ×ˢ Set.univ
theorem measurableSet_regionBetween {α : Type u_1} [] {f : α} {g : α} {s : Set α} (hf : ) (hg : ) (hs : ) :

The region between two measurable functions on a measurable set is measurable.

theorem measurableSet_region_between_oc {α : Type u_1} [] {f : α} {g : α} {s : Set α} (hf : ) (hg : ) (hs : ) :
MeasurableSet {p : α × | p.1 s p.2 Set.Ioc (f p.1) (g p.1)}

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.

theorem measurableSet_region_between_co {α : Type u_1} [] {f : α} {g : α} {s : Set α} (hf : ) (hg : ) (hs : ) :
MeasurableSet {p : α × | p.1 s p.2 Set.Ico (f p.1) (g p.1)}

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.

theorem measurableSet_region_between_cc {α : Type u_1} [] {f : α} {g : α} {s : Set α} (hf : ) (hg : ) (hs : ) :
MeasurableSet {p : α × | p.1 s p.2 Set.Icc (f p.1) (g p.1)}

The region between two measurable functions on a measurable set is measurable; a version for the region together with the graphs of both functions.

theorem measurableSet_graph {α : Type u_1} [] {f : α} (hf : ) :
MeasurableSet {p : α × | p.2 = f p.1}

The graph of a measurable function is a measurable set.

theorem volume_regionBetween_eq_lintegral' {α : Type u_1} [] {μ : } {f : α} {g : α} {s : Set α} (hf : ) (hg : ) (hs : ) :
(μ.prod MeasureTheory.volume) () = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y)μ
theorem volume_regionBetween_eq_lintegral {α : Type u_1} [] {μ : } {f : α} {g : α} {s : Set α} (hf : AEMeasurable f (μ.restrict s)) (hg : AEMeasurable g (μ.restrict s)) (hs : ) :
(μ.prod MeasureTheory.volume) () = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y)μ

The volume of the region between two almost everywhere measurable functions on a measurable set can be represented as a Lebesgue integral.

theorem nullMeasurableSet_regionBetween {α : Type u_1} [] (μ : ) {f : α} {g : α} (f_mble : ) (g_mble : ) {s : Set α} (s_mble : ) :
MeasureTheory.NullMeasurableSet {p : α × | p.1 s p.2 Set.Ioo (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

The region between two a.e.-measurable functions on a null-measurable set is null-measurable.

theorem nullMeasurableSet_region_between_oc {α : Type u_1} [] (μ : ) {f : α} {g : α} (f_mble : ) (g_mble : ) {s : Set α} (s_mble : ) :
MeasureTheory.NullMeasurableSet {p : α × | p.1 s p.2 Set.Ioc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

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.

theorem nullMeasurableSet_region_between_co {α : Type u_1} [] (μ : ) {f : α} {g : α} (f_mble : ) (g_mble : ) {s : Set α} (s_mble : ) :
MeasureTheory.NullMeasurableSet {p : α × | p.1 s p.2 Set.Ico (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

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.

theorem nullMeasurableSet_region_between_cc {α : Type u_1} [] (μ : ) {f : α} {g : α} (f_mble : ) (g_mble : ) {s : Set α} (s_mble : ) :
MeasureTheory.NullMeasurableSet {p : α × | p.1 s p.2 Set.Icc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

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.

theorem ae_restrict_of_ae_restrict_inter_Ioo {μ : } {s : } {p : } (h : ∀ (a b : ), a sb sa < b∀ᵐ (x : ) ∂μ.restrict (s Set.Ioo a b), p x) :
∀ᵐ (x : ) ∂μ.restrict s, p x

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.

theorem ae_of_mem_of_ae_of_mem_inter_Ioo {μ : } {s : } {p : } (h : ∀ (a b : ), a sb sa < b∀ᵐ (x : ) ∂μ, x s Set.Ioo a bp x) :
∀ᵐ (x : ) ∂μ, x sp x

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.