mathlib documentation

measure_theory.lebesgue_measure

Lebesgue measure on the real line

source
def measure_theory.lebesgue_length (s : set ℝ) :
ennreal

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

Equations
source
@[simp]
theorem measure_theory.lebesgue_length_empty  :
measure_theory.lebesgue_length ∅ = 0

source
@[simp]
theorem measure_theory.lebesgue_length_Ico (a b : ℝ) :
measure_theory.lebesgue_length (set.Ico a b) = ennreal.of_real (b - a)

source
theorem measure_theory.lebesgue_length_mono {s₁ s₂ : set ℝ} (h : s₁ ⊆ s₂) :
measure_theory.lebesgue_length s₁ ≤ measure_theory.lebesgue_length s₂

source
theorem measure_theory.lebesgue_length_eq_infi_Ioo (s : set ℝ) :
measure_theory.lebesgue_length s = ⨅ (a b : ℝ) (h : s ⊆ set.Ioo a b), ennreal.of_real (b - a)

source
@[simp]
theorem measure_theory.lebesgue_length_Ioo (a b : ℝ) :
measure_theory.lebesgue_length (set.Ioo a b) = ennreal.of_real (b - a)

source
theorem measure_theory.lebesgue_length_eq_infi_Icc (s : set ℝ) :
measure_theory.lebesgue_length s = ⨅ (a b : ℝ) (h : s ⊆ set.Icc a b), ennreal.of_real (b - a)

source
@[simp]
theorem measure_theory.lebesgue_length_Icc (a b : ℝ) :
measure_theory.lebesgue_length (set.Icc a b) = ennreal.of_real (b - a)

source
def measure_theory.lebesgue_outer  :
measure_theory.outer_measure ℝ

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

Equations
source
theorem measure_theory.lebesgue_outer_le_length (s : set ℝ) :
⇑measure_theory.lebesgue_outer s ≤ measure_theory.lebesgue_length s

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

source
@[simp]
theorem measure_theory.lebesgue_outer_Icc (a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Icc a b) = ennreal.of_real (b - a)

source
@[simp]
theorem measure_theory.lebesgue_outer_singleton (a : ℝ) :
⇑measure_theory.lebesgue_outer {a} = 0

source
@[simp]
theorem measure_theory.lebesgue_outer_Ico (a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Ico a b) = ennreal.of_real (b - a)

source
@[simp]
theorem measure_theory.lebesgue_outer_Ioo (a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Ioo a b) = ennreal.of_real (b - a)

source
@[simp]
theorem measure_theory.lebesgue_outer_Ioc (a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Ioc a b) = ennreal.of_real (b - a)

source
theorem measure_theory.is_lebesgue_measurable_Iio {c : ℝ} :
measure_theory.lebesgue_outer.caratheodory.is_measurable' (set.Iio c)

source
theorem measure_theory.lebesgue_outer_trim  :
measure_theory.lebesgue_outer.trim = measure_theory.lebesgue_outer

source
theorem measure_theory.borel_le_lebesgue_measurable  :
borel ℝ ≤ measure_theory.lebesgue_outer.caratheodory

source
@[instance]
def measure_theory.real.measure_space  :
measure_theory.measure_space ℝ

Lebesgue measure on the Borel sets

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

Equations
source
@[simp]
theorem measure_theory.lebesgue_to_outer_measure  :
measure_theory.measure_space.volume.to_outer_measure = measure_theory.lebesgue_outer

source
theorem real.volume_val (s : set ℝ) :
⇑measure_theory.measure_space.volume s = ⇑measure_theory.lebesgue_outer s

source
@[instance]
def real.has_no_atoms_volume  :
measure_theory.has_no_atoms measure_theory.measure_space.volume

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_interval {a b : ℝ} :
⇑measure_theory.measure_space.volume (set.interval a b) = ennreal.of_real (abs (b - a))

source
@[instance]
def real.locally_finite_volume  :
measure_theory.locally_finite_measure measure_theory.measure_space.volume

source
theorem real.map_volume_add_left (a : ℝ) :
⇑(measure_theory.measure.map (has_add.add a)) measure_theory.measure_space.volume = measure_theory.measure_space.volume

source
theorem real.map_volume_add_right (a : ℝ) :
⇑(measure_theory.measure.map (λ (_x : ℝ), _x + a)) measure_theory.measure_space.volume = measure_theory.measure_space.volume

source
theorem real.smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
ennreal.of_real (abs 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 (abs a⁻¹) • measure_theory.measure_space.volume

source
theorem real.smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
ennreal.of_real (abs 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 (abs a⁻¹) • measure_theory.measure_space.volume

source
@[simp]
theorem real.map_volume_neg  :
⇑(measure_theory.measure.map has_neg.neg) measure_theory.measure_space.volume = measure_theory.measure_space.volume