mathlib3 documentation

measure_theory.measure.null_measurable

Null measurable sets and complete measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Null measurable sets and functions #

A set s : set α is called null measurable (measure_theory.null_measurable_set) if it satisfies any of the following equivalent conditions:

Null measurable sets form a σ-algebra that is registered as a measurable_space instance on measure_theory.null_measurable_space α μ. We also say that f : α → β is measure_theory.null_measurable if the preimage of a measurable set is a null measurable set. In other words, f : α → β is null measurable if it is measurable as a function measure_theory.null_measurable_space α μ → β.

Complete measures #

We say that a measure μ is complete w.r.t. the measurable_space α σ-algebra (or the σ-algebra is complete w.r.t measure μ) if every set of measure zero is measurable. In this case all null measurable sets and functions are measurable.

For each measure μ, we define measure_theory.measure.completion μ to be the same measure interpreted as a measure on measure_theory.null_measurable_space α μ and prove that this is a complete measure.

Implementation notes #

We define measure_theory.null_measurable_set as @measurable_set (null_measurable_space α μ) _ so that theorems about measurable_sets like measurable_set.union can be applied to null_measurable_sets. However, these lemmas output terms of the same form @measurable_set (null_measurable_space α μ) _ _. While this is definitionally equal to the expected output null_measurable_set s μ, it looks different and may be misleading. So we copy all standard lemmas about measurable sets to the measure_theory.null_measurable_set namespace and fix the output type.

Tags #

measurable, measure, null measurable, completion

def measure_theory.null_measurable_set {α : Type u_2} [measurable_space α] (s : set α) (μ : measure_theory.measure α . "volume_tac") :
Prop

A set is called null_measurable_set if it can be approximated by a measurable set up to a set of null measure.

Equations
@[protected]
theorem measure_theory.null_measurable_set.Union {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_1} [countable ι] {s : ι set α} (h : (i : ι), measure_theory.null_measurable_set (s i) μ) :
@[protected]
theorem measure_theory.null_measurable_set.bUnion_decode₂ {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [encodable ι] ⦃f : ι set α (h : (i : ι), measure_theory.null_measurable_set (f i) μ) (n : ) :
@[protected]
theorem measure_theory.null_measurable_set.bUnion {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : ι set α} {s : set ι} (hs : s.countable) (h : (b : ι), b s measure_theory.null_measurable_set (f b) μ) :
measure_theory.null_measurable_set ( (b : ι) (H : b s), f b) μ
@[protected]
theorem measure_theory.null_measurable_set.Inter {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {ι : Sort u_1} [countable ι] {f : ι set α} (h : (i : ι), measure_theory.null_measurable_set (f i) μ) :
@[protected]
theorem measure_theory.null_measurable_set.bInter {α : Type u_2} {β : Type u_3} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : β set α} {s : set β} (hs : s.countable) (h : (b : β), b s measure_theory.null_measurable_set (f b) μ) :
measure_theory.null_measurable_set ( (b : β) (H : b s), f b) μ
@[protected, simp]
theorem measure_theory.exists_subordinate_pairwise_disjoint {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [countable ι] {s : ι set α} (h : (i : ι), measure_theory.null_measurable_set (s i) μ) (hd : pairwise (measure_theory.ae_disjoint μ on s)) :
(t : ι set α), ( (i : ι), t i s i) ( (i : ι), s i =ᵐ[μ] t i) ( (i : ι), measurable_set (t i)) pairwise (disjoint on t)

If sᵢ is a countable family of (null) measurable pairwise μ-a.e. disjoint sets, then there exists a subordinate family tᵢ ⊆ sᵢ of measurable pairwise disjoint sets such that tᵢ =ᵐ[μ] sᵢ.

theorem measure_theory.measure_Union {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [countable ι] {f : ι set α} (hn : pairwise (disjoint on f)) (h : (i : ι), measurable_set (f i)) :
μ ( (i : ι), f i) = ∑' (i : ι), μ (f i)
theorem measure_theory.measure_Union₀ {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [countable ι] {f : ι set α} (hd : pairwise (measure_theory.ae_disjoint μ on f)) (h : (i : ι), measure_theory.null_measurable_set (f i) μ) :
μ ( (i : ι), f i) = ∑' (i : ι), μ (f i)
theorem measure_theory.measure_inter_add_diff₀ {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {t : set α} (s : set α) (ht : measure_theory.null_measurable_set t μ) :
μ (s t) + μ (s \ t) = μ s

A null measurable set t is Carathéodory measurable: for any s, we have μ (s ∩ t) + μ (s \ t) = μ s.

theorem measure_theory.measure_union_add_inter₀ {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {t : set α} (s : set α) (ht : measure_theory.null_measurable_set t μ) :
μ (s t) + μ (s t) = μ s + μ t
theorem measure_theory.measure_union_add_inter₀' {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs : measure_theory.null_measurable_set s μ) (t : set α) :
μ (s t) + μ (s t) = μ s + μ t
theorem measure_theory.measure_union₀ {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (ht : measure_theory.null_measurable_set t μ) (hd : measure_theory.ae_disjoint μ s t) :
μ (s t) = μ s + μ t
theorem measure_theory.measure_union₀' {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} (hs : measure_theory.null_measurable_set s μ) (hd : measure_theory.ae_disjoint μ s t) :
μ (s t) = μ s + μ t
theorem set.finite.null_measurable_set_bUnion {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : ι set α} {s : set ι} (hs : s.finite) (h : (b : ι), b s measure_theory.null_measurable_set (f b) μ) :
measure_theory.null_measurable_set ( (b : ι) (H : b s), f b) μ
theorem finset.null_measurable_set_bUnion {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : ι set α} (s : finset ι) (h : (b : ι), b s measure_theory.null_measurable_set (f b) μ) :
measure_theory.null_measurable_set ( (b : ι) (H : b s), f b) μ
theorem set.finite.null_measurable_set_bInter {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : ι set α} {s : set ι} (hs : s.finite) (h : (b : ι), b s measure_theory.null_measurable_set (f b) μ) :
measure_theory.null_measurable_set ( (b : ι) (H : b s), f b) μ
theorem finset.null_measurable_set_bInter {ι : Type u_1} {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : ι set α} (s : finset ι) (h : (b : ι), b s measure_theory.null_measurable_set (f b) μ) :
measure_theory.null_measurable_set ( (b : ι) (H : b s), f b) μ
def measure_theory.null_measurable {α : Type u_2} {β : Type u_3} [measurable_space α] [measurable_space β] (f : α β) (μ : measure_theory.measure α . "volume_tac") :
Prop

A function f : α → β is null measurable if the preimage of a measurable set is a null measurable set.

Equations
@[protected]
theorem measurable.null_measurable {α : Type u_2} {β : Type u_3} [measurable_space α] [measurable_space β] {f : α β} {μ : measure_theory.measure α} (h : measurable f) :
@[protected]
theorem measure_theory.null_measurable.congr {α : Type u_2} {β : Type u_3} [measurable_space α] [measurable_space β] {f : α β} {μ : measure_theory.measure α} {g : α β} (hf : measure_theory.null_measurable f μ) (hg : f =ᵐ[μ] g) :
@[class]
structure measure_theory.measure.is_complete {α : Type u_2} {_x : measurable_space α} (μ : measure_theory.measure α) :
Prop

A measure is complete if every null set is also measurable. A null set is a subset of a measurable set with measure 0. Since every measure is defined as a special case of an outer measure, we can more simply state that a set s is null if μ s = 0.

Instances of this typeclass
theorem measure_theory.measurable_set_of_null {α : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [μ.is_complete] (hs : μ s = 0) :
theorem measurable.congr_ae {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} [hμ : μ.is_complete] {f g : α β} (hf : measurable f) (hfg : f =ᵐ[μ] g) :

Given a measure we can complete it to a (complete) measure on all null measurable sets.

Equations
Instances for measure_theory.measure.completion
theorem measure_theory.measure.completion_apply {α : Type u_2} {_x : measurable_space α} (μ : measure_theory.measure α) (s : set α) :
(μ.completion) s = μ s