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
tsuch thats =ᵐ[μ] t(this is used as a definition); MeasureTheory.toMeasurable μ s =ᵐ[μ] s;- there exists a measurable subset
t ⊆ ssuch thatt =ᵐ[μ] s(in this case the latter equality means thatμ (s \ t) = 0); scan be represented as a union of a measurable set and a set of measure zero;scan 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)
[MeasurableSpace α]
(_μ : Measure α := by volume_tac)
:
Type u_5
A type tag for α with MeasurableSet given by NullMeasurableSet.
Equations
Instances For
instance
MeasureTheory.NullMeasurableSpace.instInhabited
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[h : Inhabited α]
:
Inhabited (NullMeasurableSpace α μ)
Equations
instance
MeasureTheory.NullMeasurableSpace.instSubsingleton
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[h : Subsingleton α]
:
instance
MeasureTheory.NullMeasurableSpace.instMeasurableSpace
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
def
MeasureTheory.NullMeasurableSet
{α : Type u_2}
[MeasurableSpace α]
(s : Set α)
(μ : Measure α := by volume_tac)
:
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 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : MeasurableSet s)
:
theorem
MeasureTheory.nullMeasurableSet_empty
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
theorem
MeasureTheory.nullMeasurableSet_univ
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
theorem
MeasureTheory.NullMeasurableSet.of_null
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(h : μ s = 0)
:
theorem
MeasureTheory.NullMeasurableSet.compl
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(h : NullMeasurableSet s μ)
:
theorem
MeasureTheory.NullMeasurableSet.of_compl
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(h : NullMeasurableSet sᶜ μ)
:
@[simp]
theorem
MeasureTheory.NullMeasurableSet.compl_iff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
:
theorem
MeasureTheory.NullMeasurableSet.of_subsingleton
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[Subsingleton α]
:
theorem
MeasureTheory.NullMeasurableSet.congr
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(h : s =ᶠ[ae μ] t)
:
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) μ
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) μ
theorem
MeasureTheory.NullMeasurableSet.sUnion
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set (Set α)}
(hs : s.Countable)
(h : ∀ t ∈ s, NullMeasurableSet t μ)
:
NullMeasurableSet (⋃₀ s) μ
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) μ
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) μ
theorem
MeasureTheory.NullMeasurableSet.sInter
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set (Set α)}
(hs : s.Countable)
(h : ∀ t ∈ s, NullMeasurableSet t μ)
:
NullMeasurableSet (⋂₀ s) μ
@[simp]
theorem
MeasureTheory.NullMeasurableSet.union
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(ht : NullMeasurableSet t μ)
:
NullMeasurableSet (s ∪ t) μ
theorem
MeasureTheory.NullMeasurableSet.union_null
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(ht : μ t = 0)
:
NullMeasurableSet (s ∪ t) μ
@[simp]
theorem
MeasureTheory.NullMeasurableSet.inter
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(ht : NullMeasurableSet t μ)
:
NullMeasurableSet (s ∩ t) μ
@[simp]
theorem
MeasureTheory.NullMeasurableSet.diff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(ht : NullMeasurableSet t μ)
:
NullMeasurableSet (s \ t) μ
@[simp]
theorem
MeasureTheory.NullMeasurableSet.symmDiff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s₁ s₂ : Set α}
(h₁ : NullMeasurableSet s₁ μ)
(h₂ : NullMeasurableSet s₂ μ)
:
NullMeasurableSet (symmDiff s₁ s₂) μ
@[simp]
theorem
MeasureTheory.NullMeasurableSet.disjointed
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : ℕ → Set α}
(h : ∀ (i : ℕ), NullMeasurableSet (f i) μ)
(n : ℕ)
:
NullMeasurableSet (disjointed f n) μ
theorem
MeasureTheory.NullMeasurableSet.const
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
(p : Prop)
:
NullMeasurableSet {_a : α | p} μ
instance
MeasureTheory.NullMeasurableSet.instMeasurableSingletonClass
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[MeasurableSingletonClass α]
:
theorem
MeasureTheory.NullMeasurableSet.insert
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[MeasurableSingletonClass (NullMeasurableSpace α μ)]
(hs : NullMeasurableSet s μ)
(a : α)
:
NullMeasurableSet (insert a s) μ
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
theorem
MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(h : NullMeasurableSet s μ)
:
theorem
MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(h : NullMeasurableSet s μ)
:
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
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))
:
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 : MeasurableSpace α}
{μ : Measure α}
[Countable ι]
{f : ι → Set α}
(hn : Pairwise (Function.onFun Disjoint f))
(h : ∀ (i : ι), MeasurableSet (f i))
:
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) μ)
:
theorem
MeasureTheory.measure_union₀_aux
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(ht : NullMeasurableSet t μ)
(hd : AEDisjoint μ s t)
:
theorem
MeasureTheory.measure_inter_add_diff₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{t : Set α}
(s : Set α)
(ht : NullMeasurableSet t μ)
:
A null measurable set t is Carathéodory measurable: for any s, we have
μ (s ∩ t) + μ (s \ t) = μ s.
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) ≠ ⊤)
:
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.
theorem
MeasureTheory.measure_union_add_inter₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{t : Set α}
(s : Set α)
(ht : NullMeasurableSet t μ)
:
theorem
MeasureTheory.measure_union_add_inter₀'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(hs : NullMeasurableSet s μ)
(t : Set α)
:
theorem
MeasureTheory.measure_union₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(ht : NullMeasurableSet t μ)
(hd : AEDisjoint μ s t)
:
theorem
MeasureTheory.measure_union₀'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(hs : NullMeasurableSet s μ)
(hd : AEDisjoint μ s t)
:
theorem
MeasureTheory.measure_add_measure_compl₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(hs : NullMeasurableSet s μ)
:
theorem
MeasureTheory.measure_of_measure_compl_eq_zero
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(hs : μ sᶜ = 0)
:
theorem
MeasureTheory.nullMeasurableSet_singleton
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[MeasurableSingletonClass (NullMeasurableSpace α μ)]
(x : α)
:
@[simp]
theorem
MeasureTheory.nullMeasurableSet_insert
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[MeasurableSingletonClass (NullMeasurableSpace α μ)]
{a : α}
{s : Set α}
:
theorem
MeasureTheory.nullMeasurableSet_eq
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[MeasurableSingletonClass (NullMeasurableSpace α μ)]
{a : α}
:
theorem
Set.Finite.nullMeasurableSet
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
[MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)]
(hs : s.Finite)
:
theorem
Finset.nullMeasurableSet
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)]
(s : Finset α)
:
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) μ
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) μ
theorem
Set.Finite.nullMeasurableSet_sUnion
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set (Set α)}
(hs : s.Finite)
(h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ)
:
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) μ
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) μ
theorem
Set.Finite.nullMeasurableSet_sInter
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set (Set α)}
(hs : s.Finite)
(h : ∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ)
:
theorem
MeasureTheory.nullMeasurableSet_toMeasurable
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
:
NullMeasurableSet (toMeasurable μ s) μ
theorem
MeasureTheory.measure_preimage_fst_singleton_eq_tsum
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSingletonClass α]
{mβ : MeasurableSpace β}
[MeasurableSingletonClass β]
[Countable β]
(μ : Measure (α × β))
(x : α)
:
theorem
MeasureTheory.measure_preimage_snd_singleton_eq_tsum
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSingletonClass α]
{mβ : MeasurableSpace β}
[MeasurableSingletonClass β]
[Countable α]
(μ : Measure (α × β))
(y : β)
:
theorem
MeasureTheory.measure_preimage_fst_singleton_eq_sum
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSingletonClass α]
{mβ : MeasurableSpace β}
[MeasurableSingletonClass β]
[Fintype β]
(μ : Measure (α × β))
(x : α)
:
theorem
MeasureTheory.measure_preimage_snd_singleton_eq_sum
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSingletonClass α]
{mβ : MeasurableSpace β}
[MeasurableSingletonClass β]
[Fintype α]
(μ : Measure (α × β))
(y : β)
:
def
MeasureTheory.NullMeasurable
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : Measure α := by volume_tac)
:
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
theorem
Measurable.nullMeasurable
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{μ : MeasureTheory.Measure α}
(h : Measurable f)
:
theorem
MeasureTheory.NullMeasurable.measurable'
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{μ : Measure α}
(h : NullMeasurable f μ)
:
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) μ
theorem
MeasureTheory.NullMeasurable.congr
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{μ : Measure α}
{g : α → β}
(hf : NullMeasurable f μ)
(hg : f =ᶠ[ae μ] g)
:
NullMeasurable g μ
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
theorem
MeasureTheory.Measure.isComplete_iff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
theorem
MeasureTheory.Measure.IsComplete.out
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
(h : μ.IsComplete)
(s : Set α)
:
μ s = 0 → MeasurableSet s
theorem
MeasureTheory.measurableSet_of_null
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[μ.IsComplete]
(hs : μ s = 0)
:
theorem
MeasureTheory.NullMeasurableSet.measurable_of_complete
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(hs : NullMeasurableSet s μ)
[μ.IsComplete]
:
theorem
MeasureTheory.NullMeasurable.measurable_of_complete
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
[μ.IsComplete]
{_m1 : MeasurableSpace β}
{f : α → β}
(hf : NullMeasurable f μ)
:
theorem
Measurable.congr_ae
{α : Type u_5}
{β : Type u_6}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[_hμ : μ.IsComplete]
{f g : α → β}
(hf : Measurable f)
(hfg : f =ᵐ[μ] g)
:
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
instance
MeasureTheory.Measure.completion.isComplete
{α : Type u_2}
{_m : MeasurableSpace α}
(μ : Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.coe_completion
{α : Type u_2}
{x✝ : MeasurableSpace α}
(μ : Measure α)
:
theorem
MeasureTheory.Measure.completion_apply
{α : Type u_2}
{x✝ : MeasurableSpace α}
(μ : Measure α)
(s : Set α)
:
@[simp]
theorem
MeasureTheory.Measure.ae_completion
{α : Type u_2}
{x✝ : MeasurableSpace α}
(μ : Measure α)
: