mathlib documentation

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
theorem measure_theory.lebesgue_length_subadditive {a b : } {c d : } (ss : set.Icc a b ⋃ (i : ), set.Ioo (c i) (d i)) :
ennreal.of_real (b - a) ∑' (i : ), ennreal.of_real (d i - c i)

Definition of the Lebesgue measure and lengths of intervals

@[instance]

Lebesgue measure on the Borel sets

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

Equations

Volume of a box in ℝⁿ

theorem real.volume_Icc_pi {ι : Type u_1} [fintype ι] {a b : ι → } :

@[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 = ∏ (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 filter.eventually.volume_pos_of_nhds_real {p : → Prop} {a : } (h : ∀ᶠ (x : ) in 𝓝 a, p x) :