# mathlibdocumentation

measure_theory.lebesgue_measure

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

### Preliminary definitions #

Length of an interval. This is the largest monotonic function which correctly measures all intervals.

Equations
@[simp]
@[simp]
theorem measure_theory.lebesgue_length_mono {s₁ s₂ : set } (h : s₁ s₂) :
theorem measure_theory.lebesgue_length_eq_infi_Ioo (s : set ) :
= ⨅ (a b : ) (h : s b), ennreal.of_real (b - a)
@[simp]
theorem measure_theory.lebesgue_length_eq_infi_Icc (s : set ) :
= ⨅ (a b : ) (h : s b), ennreal.of_real (b - a)
@[simp]

The Lebesgue outer measure, as an outer measure of ℝ.

Equations
theorem measure_theory.lebesgue_length_subadditive {a b : } {c d : } (ss : b ⋃ (i : ), set.Ioo (c i) (d i)) :
ennreal.of_real (b - a) ∑' (i : ), ennreal.of_real (d i - c i)
@[simp]
@[simp]
@[simp]
@[simp]

### Definition of the Lebesgue measure and lengths of intervals #

@[protected, instance]

Lebesgue measure on the Borel sets

The outer Lebesgue measure is the completion of this measure. (TODO: proof this)

Equations
@[protected, instance]
@[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]
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]

### Volume of a box in ℝⁿ#

theorem real.volume_Icc_pi {ι : Type u_1} [fintype ι] {a b : ι → } :
= ∏ (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) :
= ∏ (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))) = ∏ (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 = ∏ (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))) = ∏ (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 = ∏ (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))) = ∏ (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 = ∏ (i : ι), (b i - a i)

### Images of the Lebesgue measure under translation/multiplication/... #

theorem real.smul_map_volume_mul_left {a : } (h : a 0) :
theorem real.map_volume_mul_left {a : } (h : a 0) :
theorem real.smul_map_volume_mul_right {a : } (h : a 0) :
theorem real.map_volume_mul_right {a : } (h : a 0) :
theorem filter.eventually.volume_pos_of_nhds_real {p : → Prop} {a : } (h : ∀ᶠ (x : ) in 𝓝 a, p x) :
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 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 volume_region_between_eq_integral' {α : Type u_1} {μ : measure_theory.measure α} {f g : α → } {s : set α} (f_int : μ) (g_int : μ) (hs : measurable_set s) (hfg : f ≤ᵐ[μ.restrict s] g) :
= ennreal.of_real ( (y : α) in s, (g - f) y μ)
theorem volume_region_between_eq_integral {α : Type u_1} {μ : measure_theory.measure α} {f g : α → } {s : set α} (f_int : μ) (g_int : μ) (hs : measurable_set s) (hfg : ∀ (x : α), x sf x g x) :
= 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.