mathlib documentation

measure_theory.measure.lebesgue

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

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

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.

theorem real.volume_val (s : set ℝ) :

⇑measure_theory.measure_space.volume s = ⇑(stieltjes_function.id.measure) s

@[simp]

theorem real.volume_Ico {a b : ℝ} :

⇑measure_theory.measure_space.volume (set.Ico a b) = ennreal.of_real (b - a)

@[simp]

theorem real.volume_Icc {a b : ℝ} :

⇑measure_theory.measure_space.volume (set.Icc a b) = ennreal.of_real (b - a)

@[simp]

theorem real.volume_Ioo {a b : ℝ} :

⇑measure_theory.measure_space.volume (set.Ioo a b) = ennreal.of_real (b - a)

@[simp]

theorem real.volume_Ioc {a b : ℝ} :

⇑measure_theory.measure_space.volume (set.Ioc a b) = ennreal.of_real (b - a)

@[simp]

theorem real.volume_singleton {a : ℝ} :

⇑measure_theory.measure_space.volume {a} = 0

@[simp]

theorem real.volume_univ :

⇑measure_theory.measure_space.volume set.univ = ⊤

@[simp]

theorem real.volume_ball (a r : ℝ) :

⇑measure_theory.measure_space.volume (metric.ball a r) = ennreal.of_real (2 * r)

@[simp]

theorem real.volume_closed_ball (a r : ℝ) :

⇑measure_theory.measure_space.volume (metric.closed_ball a r) = ennreal.of_real (2 * r)

@[simp]

theorem real.volume_emetric_ball (a : ℝ) (r : ennreal) :

⇑measure_theory.measure_space.volume (emetric.ball a r) = 2 * r

@[simp]

theorem real.volume_emetric_closed_ball (a : ℝ) (r : ennreal) :

⇑measure_theory.measure_space.volume (emetric.closed_ball a r) = 2 * r

@[protected, instance]

def real.has_no_atoms_volume :

measure_theory.has_no_atoms measure_theory.measure_space.volume

@[simp]

theorem real.volume_interval {a b : ℝ} :

⇑measure_theory.measure_space.volume (set.uIcc a b) = ennreal.of_real |b - a|

@[simp]

theorem real.volume_Ioi {a : ℝ} :

⇑measure_theory.measure_space.volume (set.Ioi a) = ⊤

@[simp]

theorem real.volume_Ici {a : ℝ} :

⇑measure_theory.measure_space.volume (set.Ici a) = ⊤

@[simp]

theorem real.volume_Iio {a : ℝ} :

⇑measure_theory.measure_space.volume (set.Iio a) = ⊤

@[simp]

theorem real.volume_Iic {a : ℝ} :

⇑measure_theory.measure_space.volume (set.Iic a) = ⊤

@[protected, instance]

def real.locally_finite_volume :

measure_theory.is_locally_finite_measure measure_theory.measure_space.volume

@[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))

@[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))

@[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))

@[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))

theorem real.volume_le_diam (s : set ℝ) :

⇑measure_theory.measure_space.volume s ≤ emetric.diam s

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 `ℝⁿ` #

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

@[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)

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

⇑measure_theory.measure_space.volume (metric.ball a r) = ennreal.of_real ((2 * r) ^ fintype.card ι)

@[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 ι)

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

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

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

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

@[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

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

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

@[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 ℝⁿ #

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

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.

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.

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.

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

set (α × ℝ)

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

Equations

region_between f g s = {p : α × ℝ | p.fst ∈ s ∧ p.snd ∈ set.Ioo (f p.fst) (g p.fst)}

theorem region_between_subset {α : Type u_1} (f g : α → ℝ) (s : set α) :

region_between f g s ⊆ s ×ˢ set.univ

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.

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.

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.

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.

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.

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) ∂μ

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.

theorem volume_region_between_eq_integral' {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f g : α → ℝ} {s : set α} [measure_theory.sigma_finite μ] (f_int : measure_theory.integrable_on f s μ) (g_int : measure_theory.integrable_on g s μ) (hs : measurable_set s) (hfg : f ≤ᵐ[μ.restrict s] g) :

⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ennreal.of_real (∫ (y : α) in s, (g - f) y ∂μ)

theorem volume_region_between_eq_integral {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f g : α → ℝ} {s : set α} [measure_theory.sigma_finite μ] (f_int : measure_theory.integrable_on f s μ) (g_int : measure_theory.integrable_on g s μ) (hs : measurable_set s) (hfg : ∀ (x : α), x ∈ s → f x ≤ g x) :

⇑(μ.prod measure_theory.measure_space.volume) (region_between f g s) = ennreal.of_real (∫ (y : α) in s, (g - f) y ∂μ)

If two functions are integrable on a measurable set, and one function is less than or equal to the other on that set, then the volume of the region between the two functions can be represented as an integral.

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.

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.