# 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 `MeasurableSet`s like `MeasurableSet.union` can be applied to `NullMeasurableSet`s. 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

source
def MeasureTheory.NullMeasurableSpace (α : Type u_5) [MeasurableSpace α] (_μ : Measure α := by volume_tac) :
Type u_5

A type tag for `α` with `MeasurableSet` given by `NullMeasurableSet`.

Equations

- MeasureTheory.NullMeasurableSpace α _μ = α

Instances For

source
instance MeasureTheory.NullMeasurableSpace.instInhabited {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [h : Inhabited α] :
Inhabited (NullMeasurableSpace α μ)
Equations

- MeasureTheory.NullMeasurableSpace.instInhabited = h

source
instance MeasureTheory.NullMeasurableSpace.instSubsingleton {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [h : Subsingleton α] :
Subsingleton (NullMeasurableSpace α μ)
source
instance MeasureTheory.NullMeasurableSpace.instMeasurableSpace {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} :
MeasurableSpace (NullMeasurableSpace α μ)
Equations

- MeasureTheory.NullMeasurableSpace.instMeasurableSpace = eventuallyMeasurableSpace inferInstance (MeasureTheory.ae μ)

source
def MeasureTheory.NullMeasurableSet {α : Type u_2} [MeasurableSpace α] (s : Set α) (μ : Measure α := by volume_tac) :
Prop

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

Equations

- MeasureTheory.NullMeasurableSet s μ = MeasurableSet s

Instances For

source
@[simp]
theorem MeasurableSet.nullMeasurableSet {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h : MeasurableSet s) :
MeasureTheory.NullMeasurableSet s μ
source
theorem MeasureTheory.nullMeasurableSet_empty {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} :
NullMeasurableSet ∅ μ
source
theorem MeasureTheory.nullMeasurableSet_univ {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} :
NullMeasurableSet Set.univ μ
source
theorem MeasureTheory.NullMeasurableSet.of_null {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : μ s = 0) :
NullMeasurableSet s μ
source
theorem MeasureTheory.NullMeasurableSet.compl {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s μ) :
NullMeasurableSet s ᶜ μ
source
theorem MeasureTheory.NullMeasurableSet.of_compl {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s ᶜ μ) :
NullMeasurableSet s μ
source
@[simp]
theorem MeasureTheory.NullMeasurableSet.compl_iff {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} :
NullMeasurableSet s ᶜ μ ↔ NullMeasurableSet s μ
source
theorem MeasureTheory.NullMeasurableSet.of_subsingleton {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [Subsingleton α] :
NullMeasurableSet s μ
source
theorem MeasureTheory.NullMeasurableSet.congr {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (h : s =ᶠ[ae μ] t) :
NullMeasurableSet t μ
source
theorem MeasureTheory.NullMeasurableSet.iUnion {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {ι : Sort u_5} [Countable ι] {s : ι → Set α} (h : ∀ (i : ι), NullMeasurableSet (s i) μ) :
NullMeasurableSet (⋃ (i : ι), s i) μ
source
theorem MeasureTheory.NullMeasurableSet.biUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {f : ι → Set α} {s : Set ι} (hs : s.Countable) (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) :
NullMeasurableSet (⋃ b ∈ s, f b) μ
source
theorem MeasureTheory.NullMeasurableSet.sUnion {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, NullMeasurableSet t μ) :
NullMeasurableSet (⋃₀ s) μ
source
theorem MeasureTheory.NullMeasurableSet.iInter {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {ι : Sort u_5} [Countable ι] {f : ι → Set α} (h : ∀ (i : ι), NullMeasurableSet (f i) μ) :
NullMeasurableSet (⋂ (i : ι), f i) μ
source
theorem MeasureTheory.NullMeasurableSet.biInter {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {μ : Measure α} {f : β → Set α} {s : Set β} (hs : s.Countable) (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) :
NullMeasurableSet (⋂ b ∈ s, f b) μ
source
theorem MeasureTheory.NullMeasurableSet.sInter {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, NullMeasurableSet t μ) :
NullMeasurableSet (⋂₀ s) μ
source
@[simp]
theorem MeasureTheory.NullMeasurableSet.union {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) :
NullMeasurableSet (s ∪ t) μ
source
theorem MeasureTheory.NullMeasurableSet.union_null {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : μ t = 0) :
NullMeasurableSet (s ∪ t) μ
source
@[simp]
theorem MeasureTheory.NullMeasurableSet.inter {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) :
NullMeasurableSet (s ∩ t) μ
source
@[simp]
theorem MeasureTheory.NullMeasurableSet.diff {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) :
NullMeasurableSet (s \ t) μ
source
@[simp]
theorem MeasureTheory.NullMeasurableSet.symmDiff {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h₁ : NullMeasurableSet s₁ μ) (h₂ : NullMeasurableSet s₂ μ) :
NullMeasurableSet (symmDiff s₁ s₂) μ
source
@[simp]
theorem MeasureTheory.NullMeasurableSet.disjointed {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {f : ℕ → Set α} (h : ∀ (i : ℕ), NullMeasurableSet (f i) μ) (n : ℕ) :
NullMeasurableSet (disjointed f n) μ
source
theorem MeasureTheory.NullMeasurableSet.const {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} (p : Prop) :
NullMeasurableSet {_a : α | p} μ
source
instance MeasureTheory.NullMeasurableSet.instMeasurableSingletonClass {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [MeasurableSingletonClass α] :
MeasurableSingletonClass (NullMeasurableSpace α μ)
source
theorem MeasureTheory.NullMeasurableSet.insert {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [MeasurableSingletonClass (NullMeasurableSpace α μ)] (hs : NullMeasurableSet s μ) (a : α) :
NullMeasurableSet (insert a s) μ
source
theorem MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s μ) :
∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
source
theorem MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s μ) :
toMeasurable μ s =ᶠ[ae μ] s
source
theorem MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s μ) :
(toMeasurable μ s ᶜ)ᶜ =ᶠ[ae μ] s
source
theorem MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s μ) :
∃ t ⊆ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
source
theorem MeasureTheory.exists_subordinate_pairwise_disjoint {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [Countable ι] {s : ι → Set α} (h : ∀ (i : ι), NullMeasurableSet (s i) μ) (hd : Pairwise (Function.onFun (AEDisjoint μ) s)) :
∃ (t : ι → Set α), (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Function.onFun Disjoint 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ᵢ`.

source
theorem MeasureTheory.measure_iUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [Countable ι] {f : ι → Set α} (hn : Pairwise (Function.onFun Disjoint f)) (h : ∀ (i : ι), MeasurableSet (f i)) :
μ (⋃ (i : ι), f i) = ∑' (i : ι), μ (f i)
source
theorem MeasureTheory.measure_iUnion₀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [Countable ι] {f : ι → Set α} (hd : Pairwise (Function.onFun (AEDisjoint μ) f)) (h : ∀ (i : ι), NullMeasurableSet (f i) μ) :
μ (⋃ (i : ι), f i) = ∑' (i : ι), μ (f i)
source
theorem MeasureTheory.measure_union₀_aux {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (hd : AEDisjoint μ s t) :
μ (s ∪ t) = μ s + μ t
source
theorem MeasureTheory.measure_inter_add_diff₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : NullMeasurableSet 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`.

source
theorem MeasureTheory.measure_diff_symm {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (h : μ s = μ t) (hfin : μ (s ∩ t) ≠ ⊤) :
μ (s \ t) = μ (t \ s)

If `s` and `t` are null measurable sets of equal measure and their intersection has finite measure, then `s \ t` and `t \ s` have equal measures too.

source
theorem MeasureTheory.measure_union_add_inter₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : NullMeasurableSet t μ) :
μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
source
theorem MeasureTheory.measure_union_add_inter₀' {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) (t : Set α) :
μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
source
theorem MeasureTheory.measure_union₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (ht : NullMeasurableSet t μ) (hd : AEDisjoint μ s t) :
μ (s ∪ t) = μ s + μ t
source
theorem MeasureTheory.measure_union₀' {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (hd : AEDisjoint μ s t) :
μ (s ∪ t) = μ s + μ t
source
theorem MeasureTheory.measure_add_measure_compl₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) :
μ s + μ s ᶜ = μ Set.univ
source
theorem MeasureTheory.measure_of_measure_compl_eq_zero {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : μ s ᶜ = 0) :
μ s = μ Set.univ
source
theorem MeasureTheory.nullMeasurableSet_singleton {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [MeasurableSingletonClass (NullMeasurableSpace α μ)] (x : α) :
NullMeasurableSet {x} μ
source
@[simp]
theorem MeasureTheory.nullMeasurableSet_insert {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [MeasurableSingletonClass (NullMeasurableSpace α μ)] {a : α} {s : Set α} :
NullMeasurableSet (insert a s) μ ↔ NullMeasurableSet s μ
source
theorem MeasureTheory.nullMeasurableSet_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} [MeasurableSingletonClass (NullMeasurableSpace α μ)] {a : α} :
NullMeasurableSet {x : α | x = a} μ
source
theorem Set.Finite.nullMeasurableSet {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)] (hs : s.Finite) :
MeasureTheory.NullMeasurableSet s μ
source
theorem Finset.nullMeasurableSet {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)] (s : Finset α) :
MeasureTheory.NullMeasurableSet (↑s) μ
source
theorem Set.Finite.nullMeasurableSet_biUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} {s : Set ι} (hs : s.Finite) (h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) :
MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
source
theorem Finset.nullMeasurableSet_biUnion {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} (s : Finset ι) (h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) :
MeasureTheory.NullMeasurableSet (⋃ b ∈ s, f b) μ
source
theorem Set.Finite.nullMeasurableSet_sUnion {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} (hs : s.Finite) (h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ) :
MeasureTheory.NullMeasurableSet (⋃₀ s) μ
source
theorem Set.Finite.nullMeasurableSet_biInter {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} {s : Set ι} (hs : s.Finite) (h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) :
MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
source
theorem Finset.nullMeasurableSet_biInter {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} (s : Finset ι) (h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) :
MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
source
theorem Set.Finite.nullMeasurableSet_sInter {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} (hs : s.Finite) (h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ) :
MeasureTheory.NullMeasurableSet (⋂₀ s) μ
source
theorem MeasureTheory.nullMeasurableSet_toMeasurable {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} :
NullMeasurableSet (toMeasurable μ s) μ
source
theorem MeasureTheory.measure_preimage_fst_singleton_eq_tsum {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} [MeasurableSingletonClass β] [Countable β] (μ : Measure (α × β)) (x : α) :
μ (Prod.fst ⁻¹' {x}) = ∑' (y : β), μ {(x, y)}
source
theorem MeasureTheory.measure_preimage_snd_singleton_eq_tsum {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} [MeasurableSingletonClass β] [Countable α] (μ : Measure (α × β)) (y : β) :
μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}
source
theorem MeasureTheory.measure_preimage_fst_singleton_eq_sum {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} [MeasurableSingletonClass β] [Fintype β] (μ : Measure (α × β)) (x : α) :
μ (Prod.fst ⁻¹' {x}) = ∑ y : β, μ {(x, y)}
source
theorem MeasureTheory.measure_preimage_snd_singleton_eq_sum {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} [MeasurableSingletonClass β] [Fintype α] (μ : Measure (α × β)) (y : β) :
μ (Prod.snd ⁻¹' {y}) = ∑ x : α, μ {(x, y)}
source
def MeasureTheory.NullMeasurable {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μ : Measure α := by volume_tac) :
Prop

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

Equations

- MeasureTheory.NullMeasurable f μ = ∀ ⦃s : Set β⦄, MeasurableSet s → MeasureTheory.NullMeasurableSet (f ⁻¹' s) μ

Instances For

source
theorem Measurable.nullMeasurable {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} (h : Measurable f) :
MeasureTheory.NullMeasurable f μ
source
theorem MeasureTheory.NullMeasurable.measurable' {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {μ : Measure α} (h : NullMeasurable f μ) :
Measurable f
source
theorem MeasureTheory.Measurable.comp_nullMeasurable {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {μ : Measure α} {g : β → γ} (hg : Measurable g) (hf : NullMeasurable f μ) :
NullMeasurable (g ∘ f) μ
source
theorem MeasureTheory.NullMeasurable.congr {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {μ : Measure α} {g : α → β} (hf : NullMeasurable f μ) (hg : f =ᶠ[ae μ] g) :
NullMeasurable g μ
source
class MeasureTheory.Measure.IsComplete {α : Type u_2} {x✝ : MeasurableSpace α} (μ : 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`.

- out' (s : Set α) : μ s = 0 → MeasurableSet s

Instances

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

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

Equations

- μ.completion = { toOuterMeasure := μ.toOuterMeasure, m_iUnion := ⋯, trim_le := ⋯ }

Instances For

source
instance MeasureTheory.Measure.completion.isComplete {α : Type u_2} {_m : MeasurableSpace α} (μ : Measure α) :
μ.completion.IsComplete
source
@[simp]
theorem MeasureTheory.Measure.coe_completion {α : Type u_2} {x✝ : MeasurableSpace α} (μ : Measure α) :
⇑μ.completion = ⇑μ
source
theorem MeasureTheory.Measure.completion_apply {α : Type u_2} {x✝ : MeasurableSpace α} (μ : Measure α) (s : Set α) :
μ.completion s = μ s
source
@[simp]
theorem MeasureTheory.Measure.ae_completion {α : Type u_2} {x✝ : MeasurableSpace α} (μ : Measure α) :
ae μ.completion = ae μ