Lebesgue measure on the real line
Length of an interval. This is the largest monotonic function which correctly measures all intervals.
Equations
- measure_theory.lebesgue_length s = ⨅ (a b : ℝ) (h : s ⊆ set.Ico a b), ennreal.of_real (b - a)
@[simp]
theorem
measure_theory.lebesgue_length_Ico
(a b : ℝ) :
measure_theory.lebesgue_length (set.Ico a b) = ennreal.of_real (b - a)
theorem
measure_theory.lebesgue_length_mono
{s₁ s₂ : set ℝ} :
s₁ ⊆ s₂ → measure_theory.lebesgue_length s₁ ≤ measure_theory.lebesgue_length s₂
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)
@[simp]
theorem
measure_theory.lebesgue_length_Ioo
(a b : ℝ) :
measure_theory.lebesgue_length (set.Ioo a b) = ennreal.of_real (b - a)
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)
@[simp]
theorem
measure_theory.lebesgue_length_Icc
(a b : ℝ) :
measure_theory.lebesgue_length (set.Icc a b) = ennreal.of_real (b - a)
The Lebesgue outer measure, as an outer measure of ℝ.
theorem
measure_theory.lebesgue_length_subadditive
{a b : ℝ}
{c d : ℕ → ℝ} :
(set.Icc a b ⊆ ⋃ (i : ℕ), set.Ioo (c i) (d i)) → (ennreal.of_real (b - a) ≤ ∑' (i : ℕ), ennreal.of_real (d i - c i))
@[simp]
theorem
measure_theory.lebesgue_outer_Icc
(a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Icc a b) = ennreal.of_real (b - a)
@[simp]
@[simp]
theorem
measure_theory.lebesgue_outer_Ico
(a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Ico a b) = ennreal.of_real (b - a)
@[simp]
theorem
measure_theory.lebesgue_outer_Ioo
(a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Ioo a b) = ennreal.of_real (b - a)
@[simp]
theorem
measure_theory.lebesgue_outer_Ioc
(a b : ℝ) :
⇑measure_theory.lebesgue_outer (set.Ioc a b) = ennreal.of_real (b - a)
@[instance]
Lebesgue measure on the Borel sets
The outer Lebesgue measure is the completion of this measure. (TODO: proof this)
Equations
- measure_theory.real.measure_space = {to_measurable_space := real.measurable_space, volume := {to_outer_measure := measure_theory.lebesgue_outer, m_Union := measure_theory.real.measure_space._proof_1, trimmed := measure_theory.lebesgue_outer_trim}}
@[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]
@[simp]
theorem
real.volume_interval
{a b : ℝ} :
⇑measure_theory.measure_space.volume (set.interval a b) = ennreal.of_real (abs (b - a))