# mathlib3documentation

measure_theory.measure.lebesgue.basic

# Lebesgue measure on the real line and on ℝⁿ#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

More properties of the Lebesgue measure are deduced from this in lebesgue.eq_haar.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.

theorem real.volume_val (s : set ) :
@[simp]
theorem real.volume_Ico {a b : } :
@[simp]
theorem real.volume_Icc {a b : } :
@[simp]
theorem real.volume_Ioo {a b : } :
@[simp]
theorem real.volume_Ioc {a b : } :
@[simp]
theorem real.volume_singleton {a : } :
@[simp]
@[simp]
theorem real.volume_ball (a r : ) :
@[simp]
theorem real.volume_closed_ball (a r : ) :
@[simp]
theorem real.volume_emetric_ball (a : ) (r : ennreal) :
@[simp]
@[protected, instance]
@[simp]
theorem real.volume_interval {a b : } :
@[simp]
theorem real.volume_Ioi {a : } :
@[simp]
theorem real.volume_Ici {a : } :
@[simp]
theorem real.volume_Iio {a : } :
@[simp]
theorem real.volume_Iic {a : } :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem real.volume_le_diam (s : set ) :

### Volume of a box in ℝⁿ#

theorem real.volume_Icc_pi {ι : Type u_1} [fintype ι] {a b : ι } :
= finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem real.volume_Icc_pi_to_real {ι : Type u_1} [fintype ι] {a b : ι } (h : a b) :
= finset.univ.prod (λ (i : ι), b i - a i)
theorem real.volume_pi_Ioo {ι : Type u_1} [fintype ι] {a b : ι } :
measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioo (a i) (b i))) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem real.volume_pi_Ioo_to_real {ι : Type u_1} [fintype ι] {a b : ι } (h : a b) :
(measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioo (a i) (b i)))).to_real = finset.univ.prod (λ (i : ι), b i - a i)
theorem real.volume_pi_Ioc {ι : Type u_1} [fintype ι] {a b : ι } :
measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioc (a i) (b i))) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem real.volume_pi_Ioc_to_real {ι : Type u_1} [fintype ι] {a b : ι } (h : a b) :
(measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ioc (a i) (b i)))).to_real = finset.univ.prod (λ (i : ι), b i - a i)
theorem real.volume_pi_Ico {ι : Type u_1} [fintype ι] {a b : ι } :
measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ico (a i) (b i))) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
@[simp]
theorem real.volume_pi_Ico_to_real {ι : Type u_1} [fintype ι] {a b : ι } (h : a b) :
(measure_theory.measure_space.volume (set.univ.pi (λ (i : ι), set.Ico (a i) (b i)))).to_real = finset.univ.prod (λ (i : ι), b i - a i)
@[simp]
theorem real.volume_pi_ball {ι : Type u_1} [fintype ι] (a : ι ) {r : } (hr : 0 < r) :
= ennreal.of_real ((2 * r) ^
@[simp]
theorem real.volume_pi_closed_ball {ι : Type u_1} [fintype ι] (a : ι ) {r : } (hr : 0 r) :
theorem real.volume_pi_le_prod_diam {ι : Type u_1} [fintype ι] (s : set )) :
finset.univ.prod (λ (i : ι), emetric.diam '' s))
theorem real.volume_pi_le_diam_pow {ι : Type u_1} [fintype ι] (s : set )) :

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

@[simp]
theorem real.volume_preimage_mul_left {a : } (h : a 0) (s : set ) :
theorem real.smul_map_volume_mul_right {a : } (h : a 0) :
theorem real.map_volume_mul_right {a : } (h : a 0) :
@[simp]
theorem real.volume_preimage_mul_right {a : } (h : a 0) (s : set ) :

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

theorem real.smul_map_diagonal_volume_pi {ι : Type u_1} [fintype ι] [decidable_eq ι] {D : ι } (h : .det 0) :

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.

theorem real.map_matrix_volume_pi_eq_smul_volume_pi {ι : Type u_1} [fintype ι] [decidable_eq ι] {M : ι } (hM : M.det 0) :

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

theorem real.map_linear_map_volume_pi_eq_smul_volume_pi {ι : Type u_1} [fintype ι] {f : ) →ₗ[] ι } (hf : 0) :

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

def region_between {α : Type u_1} (f g : α ) (s : set α) :
set × )

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

Equations
theorem region_between_subset {α : Type u_1} (f g : α ) (s : set α) :
s
theorem measurable_set_region_between {α : Type u_1} {f g : α } {s : set α} (hf : measurable f) (hg : measurable g) (hs : measurable_set s) :

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

theorem measurable_set_region_between_oc {α : Type u_1} {f g : α } {s : set α} (hf : measurable f) (hg : measurable g) (hs : measurable_set s) :
measurable_set {p : α × | p.fst s p.snd set.Ioc (f p.fst) (g p.fst)}

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 measurable_set_region_between_co {α : Type u_1} {f g : α } {s : set α} (hf : measurable f) (hg : measurable g) (hs : measurable_set s) :
measurable_set {p : α × | p.fst s p.snd set.Ico (f p.fst) (g p.fst)}

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 measurable_set_region_between_cc {α : Type u_1} {f g : α } {s : set α} (hf : measurable f) (hg : measurable g) (hs : measurable_set s) :
measurable_set {p : α × | p.fst s p.snd set.Icc (f p.fst) (g p.fst)}

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 measurable_set_graph {α : Type u_1} {f : α } (hf : measurable f) :
measurable_set {p : α × | p.snd = f p.fst}

The graph of a measurable function is a measurable set.

theorem volume_region_between_eq_lintegral' {α : Type u_1} {μ : measure_theory.measure α} {f g : α } {s : set α} (hf : measurable f) (hg : measurable g) (hs : measurable_set s) :
= ∫⁻ (y : α) in s, ennreal.of_real ((g - f) y) μ
theorem volume_region_between_eq_lintegral {α : Type u_1} {μ : measure_theory.measure α} {f g : α } {s : set α} (hf : (μ.restrict s)) (hg : (μ.restrict s)) (hs : measurable_set s) :
= ∫⁻ (y : α) in s, ennreal.of_real ((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 ae_restrict_of_ae_restrict_inter_Ioo {s : set } {p : Prop} (h : (a b : ), a s b s a < b (∀ᵐ (x : ) μ.restrict (s 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 : set } {p : Prop} (h : (a b : ), a s b s a < b (∀ᵐ (x : ) μ, x s b p x)) :
∀ᵐ (x : ) μ, x 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 bare membership. See also ae_restrict_of_ae_restrict_inter_Ioo.