mathlib3 documentation

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 #

source
theorem real.volume_eq_stieltjes_id  :
measure_theory.measure_space.volume = stieltjes_function.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.

source
theorem real.volume_val (s : set ℝ) :
⇑measure_theory.measure_space.volume s = ⇑(stieltjes_function.id.measure) s
source
@[simp]
theorem real.volume_Ico {a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Ico a b) = ennreal.of_real (b - a)
source
@[simp]
theorem real.volume_Icc {a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Icc a b) = ennreal.of_real (b - a)
source
@[simp]
theorem real.volume_Ioo {a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Ioo a b) = ennreal.of_real (b - a)
source
@[simp]
theorem real.volume_Ioc {a b : ℝ} :
⇑measure_theory.measure_space.volume (set.Ioc a b) = ennreal.of_real (b - a)
source
@[simp]
theorem real.volume_singleton {a : ℝ} :
⇑measure_theory.measure_space.volume {a} = 0
source
@[simp]
theorem real.volume_univ  :
⇑measure_theory.measure_space.volume set.univ = ⊤
source
@[simp]
theorem real.volume_ball (a r : ℝ) :
⇑measure_theory.measure_space.volume (metric.ball a r) = ennreal.of_real (2 * r)
source
@[simp]
theorem real.volume_closed_ball (a r : ℝ) :
⇑measure_theory.measure_space.volume (metric.closed_ball a r) = ennreal.of_real (2 * r)
source
@[simp]
theorem real.volume_emetric_ball (a : ℝ) (r : ennreal) :
⇑measure_theory.measure_space.volume (emetric.ball a r) = 2 * r
source
@[simp]
theorem real.volume_emetric_closed_ball (a : ℝ) (r : ennreal) :
⇑measure_theory.measure_space.volume (emetric.closed_ball a r) = 2 * r
source
@[protected, instance]
def real.has_no_atoms_volume  :
measure_theory.has_no_atoms measure_theory.measure_space.volume
source
@[simp]
theorem real.volume_interval {a b : ℝ} :
⇑measure_theory.measure_space.volume (set.uIcc a b) = ennreal.of_real |b - a|
source
@[simp]
theorem real.volume_Ioi {a : ℝ} :
⇑measure_theory.measure_space.volume (set.Ioi a) = ⊤
source
@[simp]
theorem real.volume_Ici {a : ℝ} :
⇑measure_theory.measure_space.volume (set.Ici a) = ⊤
source
@[simp]
theorem real.volume_Iio {a : ℝ} :
⇑measure_theory.measure_space.volume (set.Iio a) = ⊤
source
@[simp]
theorem real.volume_Iic {a : ℝ} :
⇑measure_theory.measure_space.volume (set.Iic a) = ⊤
source
@[protected, instance]
def real.locally_finite_volume  :
measure_theory.is_locally_finite_measure measure_theory.measure_space.volume
source
@[protected, instance]
def real.is_finite_measure_restrict_Icc (x y : ℝ) :
measure_theory.is_finite_measure (measure_theory.measure_space.volume.restrict (set.Icc x y))
source
@[protected, instance]
def real.is_finite_measure_restrict_Ico (x y : ℝ) :
measure_theory.is_finite_measure (measure_theory.measure_space.volume.restrict (set.Ico x y))
source
@[protected, instance]
def real.is_finite_measure_restrict_Ioc (x y : ℝ) :
measure_theory.is_finite_measure (measure_theory.measure_space.volume.restrict (set.Ioc x y))
source
@[protected, instance]
def real.is_finite_measure_restrict_Ioo (x y : ℝ) :
measure_theory.is_finite_measure (measure_theory.measure_space.volume.restrict (set.Ioo x y))
source
theorem real.volume_le_diam (s : set ℝ) :
⇑measure_theory.measure_space.volume s ≤ emetric.diam s
source
theorem filter.eventually.volume_pos_of_nhds_real {p : ℝ → Prop} {a : ℝ} (h : ∀ᶠ (x : ℝ) in nhds a, p x) :
0 < ⇑measure_theory.measure_space.volume {x : ℝ | p x}

Volume of a box in ℝⁿ #

source
theorem real.volume_Icc_pi {ι : Type u_1} [fintype ι] {a b : ι → ℝ} :
⇑measure_theory.measure_space.volume (set.Icc a b) = finset.univ.prod (λ (i : ι), ennreal.of_real (b i - a i))
source
@[simp]
theorem real.volume_Icc_pi_to_real {ι : Type u_1} [fintype ι] {a b : ι → ℝ} (h : a ≤ b) :
(⇑measure_theory.measure_space.volume (set.Icc a b)).to_real = finset.univ.prod (λ (i : ι), b i - a i)
source
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))
source
@[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)
source
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))
source
@[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)
source
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))
source
@[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)
source
@[simp]
theorem real.volume_pi_ball {ι : Type u_1} [fintype ι] (a : ι → ℝ) {r : ℝ} (hr : 0 < r) :
⇑measure_theory.measure_space.volume (metric.ball a r) = ennreal.of_real ((2 * r) ^ fintype.card ι)
source
@[simp]
theorem real.volume_pi_closed_ball {ι : Type u_1} [fintype ι] (a : ι → ℝ) {r : ℝ} (hr : 0 ≤ r) :
⇑measure_theory.measure_space.volume (metric.closed_ball a r) = ennreal.of_real ((2 * r) ^ fintype.card ι)
source
theorem real.volume_pi_le_prod_diam {ι : Type u_1} [fintype ι] (s : set (ι → ℝ)) :
⇑measure_theory.measure_space.volume s ≤ finset.univ.prod (λ (i : ι), emetric.diam (function.eval i '' s))
source
theorem real.volume_pi_le_diam_pow {ι : Type u_1} [fintype ι] (s : set (ι → ℝ)) :
⇑measure_theory.measure_space.volume s ≤ emetric.diam s ^ fintype.card ι

Images of the Lebesgue measure under multiplication in ℝ #

source
theorem real.smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
ennreal.of_real |a| • measure_theory.measure.map (has_mul.mul a) measure_theory.measure_space.volume = measure_theory.measure_space.volume
source
theorem real.map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
measure_theory.measure.map (has_mul.mul a) measure_theory.measure_space.volume = ennreal.of_real |a⁻¹| • measure_theory.measure_space.volume
source
@[simp]
theorem real.volume_preimage_mul_left {a : ℝ} (h : a ≠ 0) (s : set ℝ) :
⇑measure_theory.measure_space.volume (has_mul.mul a ⁻¹' s) = ennreal.of_real |a⁻¹| * ⇑measure_theory.measure_space.volume s
source
theorem real.smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
ennreal.of_real |a| • measure_theory.measure.map (λ (_x : ℝ), _x * a) measure_theory.measure_space.volume = measure_theory.measure_space.volume
source
theorem real.map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
measure_theory.measure.map (λ (_x : ℝ), _x * a) measure_theory.measure_space.volume = ennreal.of_real |a⁻¹| • measure_theory.measure_space.volume
source
@[simp]
theorem real.volume_preimage_mul_right {a : ℝ} (h : a ≠ 0) (s : set ℝ) :
⇑measure_theory.measure_space.volume ((λ (_x : ℝ), _x * a) ⁻¹' s) = ennreal.of_real |a⁻¹| * ⇑measure_theory.measure_space.volume s

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

source
theorem real.smul_map_diagonal_volume_pi {ι : Type u_1} [fintype ι] [decidable_eq ι] {D : ι → ℝ} (h : (matrix.diagonal D).det ≠ 0) :
ennreal.of_real |(matrix.diagonal D).det| • measure_theory.measure.map ⇑(⇑matrix.to_lin' (matrix.diagonal D)) measure_theory.measure_space.volume = measure_theory.measure_space.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).

source
theorem real.volume_preserving_transvection_struct {ι : Type u_1} [fintype ι] [decidable_eq ι] (t : matrix.transvection_struct ι ℝ) :
measure_theory.measure_preserving ⇑(⇑matrix.to_lin' t.to_matrix) measure_theory.measure_space.volume measure_theory.measure_space.volume

A transvection preserves Lebesgue measure.

source
theorem real.map_matrix_volume_pi_eq_smul_volume_pi {ι : Type u_1} [fintype ι] [decidable_eq ι] {M : matrix ι ι ℝ} (hM : M.det ≠ 0) :
measure_theory.measure.map ⇑(⇑matrix.to_lin' M) measure_theory.measure_space.volume = ennreal.of_real |(M.det)⁻¹| • measure_theory.measure_space.volume

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

source
theorem real.map_linear_map_volume_pi_eq_smul_volume_pi {ι : Type u_1} [fintype ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ} (hf : ⇑linear_map.det f ≠ 0) :
measure_theory.measure.map ⇑f measure_theory.measure_space.volume = ennreal.of_real |(⇑linear_map.det f)⁻¹| • measure_theory.measure_space.volume

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

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

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

Equations
source
theorem region_between_subset {α : Type u_1} (f g : α → ℝ) (s : set α) :
region_between f g s ⊆ s ×ˢ set.univ
source
theorem measurable_set_region_between {α : Type u_1} [measurable_space α] {f g : α → ℝ} {s : set α} (hf : measurable f) (hg : measurable g) (hs : measurable_set s) :
measurable_set (region_between f g s)

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

source
theorem measurable_set_region_between_oc {α : Type u_1} [measurable_space α] {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.

source
theorem measurable_set_region_between_co {α : Type u_1} [measurable_space α] {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.

source
theorem measurable_set_region_between_cc {α : Type u_1} [measurable_space α] {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.

source
theorem measurable_set_graph {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
measurable_set {p : α × ℝ | p.snd = f p.fst}

The graph of a measurable function is a measurable set.

source
theorem volume_region_between_eq_lintegral' {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f g : α → ℝ} {s : set α} (hf : measurable f) (hg : measurable g) (hs : measurable_set s) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ∫⁻ (y : α) in s, ennreal.of_real ((g - f) y) ∂μ
source
theorem volume_region_between_eq_lintegral {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f g : α → ℝ} {s : set α} [measure_theory.sigma_finite μ] (hf : ae_measurable f (μ.restrict s)) (hg : ae_measurable g (μ.restrict s)) (hs : measurable_set s) :
⇑(μ.prod measure_theory.measure_space.volume) (region_between f g 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.

source
theorem ae_restrict_of_ae_restrict_inter_Ioo {μ : measure_theory.measure ℝ} [measure_theory.has_no_atoms μ] {s : set ℝ} {p : ℝ → Prop} (h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < 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.

source
theorem ae_of_mem_of_ae_of_mem_inter_Ioo {μ : measure_theory.measure ℝ} [measure_theory.has_no_atoms μ] {s : set ℝ} {p : ℝ → Prop} (h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → (∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ set.Ioo a 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.