# Null measurable sets and complete measures #

## Main definitions #

### Null measurable sets and functions #

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

• there exists a measurable set t such that s =ᵐ[μ] t (this is used as a definition);
• MeasureTheory.toMeasurable μ s =ᵐ[μ] s;
• there exists a measurable subset t ⊆ s such that t =ᵐ[μ] s (in this case the latter equality means that μ (s \ t) = 0);
• s can be represented as a union of a measurable set and a set of measure zero;
• s can be represented as a difference of a measurable set and a set of measure zero.

Null measurable sets form a σ-algebra that is registered as a MeasurableSpace instance on MeasureTheory.NullMeasurableSpace α μ. We also say that f : α → β is MeasureTheory.NullMeasurable 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 MeasureTheory.NullMeasurableSpace α μ → β.

### Complete measures #

We say that a measure μ is complete w.r.t. the MeasurableSpace α σ-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 MeasureTheory.Measure.completion μ to be the same measure interpreted as a measure on MeasureTheory.NullMeasurableSpace α μ and prove that this is a complete measure.

## Implementation notes #

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

## Tags #

measurable, measure, null measurable, completion

def MeasureTheory.NullMeasurableSpace (α : Type u_5) [] (_μ : ) :
Type u_5

A type tag for α with MeasurableSet given by NullMeasurableSet.

Equations
Instances For
instance MeasureTheory.NullMeasurableSpace.instInhabited {α : Type u_2} {m0 : } {μ : } [h : ] :
Equations
• MeasureTheory.NullMeasurableSpace.instInhabited = h
instance MeasureTheory.NullMeasurableSpace.instSubsingleton {α : Type u_2} {m0 : } {μ : } [h : ] :
Equations
instance MeasureTheory.NullMeasurableSpace.instMeasurableSpace {α : Type u_2} {m0 : } {μ : } :
Equations
• One or more equations did not get rendered due to their size.
def MeasureTheory.NullMeasurableSet {α : Type u_2} [] (s : Set α) (μ : ) :

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

Equations
Instances For
@[simp]
theorem MeasurableSet.nullMeasurableSet {α : Type u_2} {m0 : } {μ : } {s : Set α} (h : ) :
theorem MeasureTheory.nullMeasurableSet_empty {α : Type u_2} {m0 : } {μ : } :
theorem MeasureTheory.NullMeasurableSet.of_null {α : Type u_2} {m0 : } {μ : } {s : Set α} (h : μ s = 0) :
theorem MeasureTheory.NullMeasurableSet.compl {α : Type u_2} {m0 : } {μ : } {s : Set α} :
theorem MeasureTheory.NullMeasurableSet.of_compl {α : Type u_2} {m0 : } {μ : } {s : Set α} :
@[simp]
theorem MeasureTheory.NullMeasurableSet.compl_iff {α : Type u_2} {m0 : } {μ : } {s : Set α} :
theorem MeasureTheory.NullMeasurableSet.of_subsingleton {α : Type u_2} {m0 : } {μ : } {s : Set α} [] :
theorem MeasureTheory.NullMeasurableSet.congr {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (h : ) :
theorem MeasureTheory.NullMeasurableSet.iUnion {α : Type u_2} {m0 : } {μ : } {ι : Sort u_5} [] {s : ιSet α} (h : ∀ (i : ι), ) :
@[deprecated Set.iUnion]
theorem MeasureTheory.NullMeasurableSet.biUnion_decode₂ {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } [] ⦃f : ιSet α (h : ∀ (i : ι), ) (n : ) :
theorem MeasureTheory.NullMeasurableSet.biUnion {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } {f : ιSet α} {s : Set ι} (hs : ) (h : bs, ) :
theorem MeasureTheory.NullMeasurableSet.sUnion {α : Type u_2} {m0 : } {μ : } {s : Set (Set α)} (hs : ) (h : ) :
theorem MeasureTheory.NullMeasurableSet.iInter {α : Type u_2} {m0 : } {μ : } {ι : Sort u_5} [] {f : ιSet α} (h : ∀ (i : ι), ) :
theorem MeasureTheory.NullMeasurableSet.biInter {α : Type u_2} {β : Type u_3} {m0 : } {μ : } {f : βSet α} {s : Set β} (hs : ) (h : bs, ) :
theorem MeasureTheory.NullMeasurableSet.sInter {α : Type u_2} {m0 : } {μ : } {s : Set (Set α)} (hs : ) (h : ) :
@[simp]
theorem MeasureTheory.NullMeasurableSet.union {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem MeasureTheory.NullMeasurableSet.union_null {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : μ t = 0) :
@[simp]
theorem MeasureTheory.NullMeasurableSet.inter {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) :
@[simp]
theorem MeasureTheory.NullMeasurableSet.diff {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) :
@[simp]
theorem MeasureTheory.NullMeasurableSet.disjointed {α : Type u_2} {m0 : } {μ : } {f : Set α} (h : ∀ (i : ), ) (n : ) :
theorem MeasureTheory.NullMeasurableSet.const {α : Type u_2} {m0 : } {μ : } (p : Prop) :
Equations
theorem MeasureTheory.NullMeasurableSet.insert {α : Type u_2} {m0 : } {μ : } {s : Set α} (hs : ) (a : α) :
theorem MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq {α : Type u_2} {m0 : } {μ : } {s : Set α} :
∃ t ⊇ s,
theorem MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq {α : Type u_2} {m0 : } {μ : } {s : Set α} :
theorem MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq {α : Type u_2} {m0 : } {μ : } {s : Set α} :
∃ t ⊆ s,
theorem MeasureTheory.exists_subordinate_pairwise_disjoint {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } [] {s : ιSet α} (h : ∀ (i : ι), ) (hd : ) :
∃ (t : ιSet α), (∀ (i : ι), t i s i) (∀ (i : ι), s i =ᶠ[] t i) (∀ (i : ι), MeasurableSet (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 MeasureTheory.measure_iUnion {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } [] {f : ιSet α} (hn : Pairwise (Disjoint on f)) (h : ∀ (i : ι), MeasurableSet (f i)) :
μ (⋃ (i : ι), f i) = ∑' (i : ι), μ (f i)
theorem MeasureTheory.measure_iUnion₀ {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } [] {f : ιSet α} (hd : ) (h : ∀ (i : ι), ) :
μ (⋃ (i : ι), f i) = ∑' (i : ι), μ (f i)
theorem MeasureTheory.measure_union₀_aux {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (ht : ) (hd : ) :
μ (s t) = μ s + μ t
theorem MeasureTheory.measure_inter_add_diff₀ {α : Type u_2} {m0 : } {μ : } {t : Set α} (s : Set α) (ht : ) :
μ (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 MeasureTheory.measure_union_add_inter₀ {α : Type u_2} {m0 : } {μ : } {t : Set α} (s : Set α) (ht : ) :
μ (s t) + μ (s t) = μ s + μ t
theorem MeasureTheory.measure_union_add_inter₀' {α : Type u_2} {m0 : } {μ : } {s : Set α} (hs : ) (t : Set α) :
μ (s t) + μ (s t) = μ s + μ t
theorem MeasureTheory.measure_union₀ {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (ht : ) (hd : ) :
μ (s t) = μ s + μ t
theorem MeasureTheory.measure_union₀' {α : Type u_2} {m0 : } {μ : } {s : Set α} {t : Set α} (hs : ) (hd : ) :
μ (s t) = μ s + μ t
theorem MeasureTheory.measure_add_measure_compl₀ {α : Type u_2} {m0 : } {μ : } {s : Set α} (hs : ) :
μ s + μ s = μ Set.univ
theorem MeasureTheory.nullMeasurableSet_singleton {α : Type u_2} {m0 : } {μ : } (x : α) :
@[simp]
theorem MeasureTheory.nullMeasurableSet_insert {α : Type u_2} {m0 : } {μ : } {a : α} {s : Set α} :
theorem MeasureTheory.nullMeasurableSet_eq {α : Type u_2} {m0 : } {μ : } {a : α} :
theorem Set.Finite.nullMeasurableSet {α : Type u_2} {m0 : } {μ : } {s : Set α} (hs : ) :
theorem Finset.nullMeasurableSet {α : Type u_2} {m0 : } {μ : } (s : ) :
theorem Set.Finite.nullMeasurableSet_biUnion {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } {f : ιSet α} {s : Set ι} (hs : ) (h : bs, ) :
theorem Finset.nullMeasurableSet_biUnion {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } {f : ιSet α} (s : ) (h : bs, ) :
theorem Set.Finite.nullMeasurableSet_sUnion {α : Type u_2} {m0 : } {μ : } {s : Set (Set α)} (hs : ) (h : ) :
theorem Set.Finite.nullMeasurableSet_biInter {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } {f : ιSet α} {s : Set ι} (hs : ) (h : bs, ) :
theorem Finset.nullMeasurableSet_biInter {ι : Type u_1} {α : Type u_2} {m0 : } {μ : } {f : ιSet α} (s : ) (h : bs, ) :
theorem Set.Finite.nullMeasurableSet_sInter {α : Type u_2} {m0 : } {μ : } {s : Set (Set α)} (hs : ) (h : ) :
theorem MeasureTheory.nullMeasurableSet_toMeasurable {α : Type u_2} {m0 : } {μ : } {s : Set α} :
def MeasureTheory.NullMeasurable {α : Type u_2} {β : Type u_3} [] [] (f : αβ) (μ : ) :

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

Equations
• = ∀ ⦃s : Set β⦄,
Instances For
theorem Measurable.nullMeasurable {α : Type u_2} {β : Type u_3} [] [] {f : αβ} {μ : } (h : ) :
theorem MeasureTheory.NullMeasurable.measurable' {α : Type u_2} {β : Type u_3} [] [] {f : αβ} {μ : } (h : ) :
theorem MeasureTheory.Measurable.comp_nullMeasurable {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] {f : αβ} {μ : } {g : βγ} (hg : ) (hf : ) :
theorem MeasureTheory.NullMeasurable.congr {α : Type u_2} {β : Type u_3} [] [] {f : αβ} {μ : } {g : αβ} (hf : ) (hg : ) :
class MeasureTheory.Measure.IsComplete {α : Type u_2} :
{x : } →

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.

• out' : ∀ (s : Set α), μ s = 0
Instances
theorem MeasureTheory.Measure.isComplete_iff {α : Type u_2} {m0 : } {μ : } :
∀ (s : Set α), μ s = 0
theorem MeasureTheory.Measure.IsComplete.out {α : Type u_2} {m0 : } {μ : } (s : Set α) :
μ s = 0
theorem MeasureTheory.measurableSet_of_null {α : Type u_2} {m0 : } {μ : } {s : Set α} (hs : μ s = 0) :
theorem MeasureTheory.NullMeasurableSet.measurable_of_complete {α : Type u_2} {m0 : } {μ : } {s : Set α} (hs : ) :
theorem MeasureTheory.NullMeasurable.measurable_of_complete {α : Type u_2} {β : Type u_3} {m0 : } {μ : } {_m1 : } {f : αβ} (hf : ) :
theorem Measurable.congr_ae {α : Type u_5} {β : Type u_6} [] [] {μ : } [_hμ : ] {f : αβ} {g : αβ} (hf : ) (hfg : ) :
def MeasureTheory.Measure.completion {α : Type u_2} :
{x : } →

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance MeasureTheory.Measure.completion.isComplete {α : Type u_2} {_m : } (μ : ) :
Equations
@[simp]
theorem MeasureTheory.Measure.coe_completion {α : Type u_2} :
∀ {x : } (μ : ), = μ
theorem MeasureTheory.Measure.completion_apply {α : Type u_2} :
∀ {x : } (μ : ) (s : Set α), = μ s
@[simp]