mathlib documentation

measure_theory.lebesgue_measure

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

Preliminary definitions #

def measure_theory.lebesgue_length (s : set ℝ) :

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

measure_theory.lebesgue_length ∅ = 0

@[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 ℝ} (h : 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)

def measure_theory.lebesgue_outer :

measure_theory.outer_measure ℝ

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

Equations

measure_theory.lebesgue_outer = measure_theory.outer_measure.of_function measure_theory.lebesgue_length measure_theory.lebesgue_length_empty

theorem measure_theory.lebesgue_outer_le_length (s : set ℝ) :

⇑measure_theory.lebesgue_outer s ≤ measure_theory.lebesgue_length s

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)

@[simp]

theorem measure_theory.lebesgue_outer_Icc (a b : ℝ) :

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

@[simp]

theorem measure_theory.lebesgue_outer_singleton (a : ℝ) :

⇑measure_theory.lebesgue_outer {a} = 0

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

theorem measure_theory.is_lebesgue_measurable_Iio {c : ℝ} :

measure_theory.lebesgue_outer.caratheodory.measurable_set' (set.Iio c)

theorem measure_theory.lebesgue_outer_trim :

measure_theory.lebesgue_outer.trim = measure_theory.lebesgue_outer

theorem measure_theory.borel_le_lebesgue_measurable :

borel ℝ ≤ measure_theory.lebesgue_outer.caratheodory

Definition of the Lebesgue measure and lengths of intervals #

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

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 measure_theory.lebesgue_to_outer_measure :

measure_theory.measure_space.volume.to_outer_measure = measure_theory.lebesgue_outer

theorem real.volume_val (s : set ℝ) :

⇑measure_theory.measure_space.volume s = ⇑measure_theory.lebesgue_outer s

@[protected, instance]

def real.has_no_atoms_volume :

measure_theory.has_no_atoms measure_theory.measure_space.volume

@[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_interval {a b : ℝ} :

⇑measure_theory.measure_space.volume (set.interval a b) = ennreal.of_real (abs (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.locally_finite_measure measure_theory.measure_space.volume

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) = ∏ (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 = ∏ (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.map_volume_add_left (a : ℝ) :

⇑(measure_theory.measure.map (has_add.add a)) measure_theory.measure_space.volume = measure_theory.measure_space.volume

theorem real.map_volume_add_right (a : ℝ) :

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

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

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

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

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

@[simp]

theorem real.map_volume_neg :

⇑(measure_theory.measure.map has_neg.neg) measure_theory.measure_space.volume = measure_theory.measure_space.volume

theorem filter.eventually.volume_pos_of_nhds_real {p : ℝ → Prop} {a : ℝ} (h : ∀ᶠ (x : ℝ) in 𝓝 a, p x) :

0 < ⇑measure_theory.measure_space.volume {x : ℝ | 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

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