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:
- there exists a measurable set
tsuch thats =ᵐ[μ] t(this is used as a definition); measure_theory.to_measurable μ 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 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
@[nolint]
def
measure_theory.null_measurable_space
(α : Type u_1)
[measurable_space α]
(μ : measure_theory.measure α . "volume_tac") :
Type u_1
A type tag for α with measurable_set given by null_measurable_set.
Equations
Instances for measure_theory.null_measurable_space
@[protected, instance]
def
measure_theory.null_measurable_space.inhabited
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[h : inhabited α] :
Equations
@[protected, instance]
def
measure_theory.null_measurable_space.subsingleton
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[h : subsingleton α] :
@[protected, instance]
def
measure_theory.null_measurable_space.measurable_space
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
Equations
- measure_theory.null_measurable_space.measurable_space = {measurable_set' := λ (s : set (measure_theory.null_measurable_space α μ)), ∃ (t : set α), measurable_set t ∧ s =ᵐ[μ] t, measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}
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
@[simp]
theorem
measurable_set.null_measurable_set
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measurable_set s) :
@[simp]
theorem
measure_theory.null_measurable_set_empty
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.null_measurable_set_univ
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
theorem
measure_theory.null_measurable_set.of_null
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : ⇑μ s = 0) :
theorem
measure_theory.null_measurable_set.compl
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measure_theory.null_measurable_set s μ) :
theorem
measure_theory.null_measurable_set.of_compl
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measure_theory.null_measurable_set sᶜ μ) :
@[simp]
theorem
measure_theory.null_measurable_set.compl_iff
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.null_measurable_set.of_subsingleton
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[subsingleton α] :
@[protected]
theorem
measure_theory.null_measurable_set.congr
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s μ)
(h : s =ᵐ[μ] t) :
@[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) μ) :
measure_theory.null_measurable_set (⋃ (i : ι), 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 : ℕ) :
measure_theory.null_measurable_set (⋃ (b : ι) (H : b ∈ encodable.decode₂ ι n), f b) μ
@[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.sUnion
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set (set α)}
(hs : s.countable)
(h : ∀ (t : set α), t ∈ s → measure_theory.null_measurable_set t μ) :
@[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) μ) :
measure_theory.null_measurable_set (⋂ (i : ι), 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]
theorem
measure_theory.null_measurable_set.sInter
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set (set α)}
(hs : s.countable)
(h : ∀ (t : set α), t ∈ s → measure_theory.null_measurable_set t μ) :
@[protected, simp]
theorem
measure_theory.null_measurable_set.union
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s μ)
(ht : measure_theory.null_measurable_set t μ) :
measure_theory.null_measurable_set (s ∪ t) μ
@[protected]
theorem
measure_theory.null_measurable_set.union_null
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s μ)
(ht : ⇑μ t = 0) :
measure_theory.null_measurable_set (s ∪ t) μ
@[protected, simp]
theorem
measure_theory.null_measurable_set.inter
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s μ)
(ht : measure_theory.null_measurable_set t μ) :
measure_theory.null_measurable_set (s ∩ t) μ
@[protected, simp]
theorem
measure_theory.null_measurable_set.diff
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s μ)
(ht : measure_theory.null_measurable_set t μ) :
measure_theory.null_measurable_set (s \ t) μ
@[protected, simp]
theorem
measure_theory.null_measurable_set.disjointed
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ℕ → set α}
(h : ∀ (i : ℕ), measure_theory.null_measurable_set (f i) μ)
(n : ℕ) :
@[protected, simp]
theorem
measure_theory.null_measurable_set.const
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
(p : Prop) :
measure_theory.null_measurable_set {a : α | p} μ
@[protected, instance]
@[protected]
theorem
measure_theory.null_measurable_set.insert
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[measurable_singleton_class (measure_theory.null_measurable_space α μ)]
(hs : measure_theory.null_measurable_set s μ)
(a : α) :
theorem
measure_theory.null_measurable_set.exists_measurable_superset_ae_eq
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measure_theory.null_measurable_set s μ) :
theorem
measure_theory.null_measurable_set.to_measurable_ae_eq
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measure_theory.null_measurable_set s μ) :
measure_theory.to_measurable μ s =ᵐ[μ] s
theorem
measure_theory.null_measurable_set.compl_to_measurable_compl_ae_eq
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measure_theory.null_measurable_set s μ) :
(measure_theory.to_measurable μ sᶜ)ᶜ =ᵐ[μ] s
theorem
measure_theory.null_measurable_set.exists_measurable_subset_ae_eq
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measure_theory.null_measurable_set s μ) :
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)) :
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 α}
(hd : pairwise (measure_theory.ae_disjoint μ on f))
(h : ∀ (i : ι), measure_theory.null_measurable_set (f i) μ) :
theorem
measure_theory.measure_union₀_aux
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s μ)
(ht : measure_theory.null_measurable_set t μ)
(hd : measure_theory.ae_disjoint μ s t) :
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 μ) :
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 μ) :
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 α) :
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) :
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) :
theorem
measure_theory.measure_add_measure_compl₀
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.null_measurable_set s μ) :
theorem
measure_theory.null_measurable_set_singleton
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[measurable_singleton_class (measure_theory.null_measurable_space α μ)]
(x : α) :
@[simp]
theorem
measure_theory.null_measurable_set_insert
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[measurable_singleton_class (measure_theory.null_measurable_space α μ)]
{a : α}
{s : set α} :
theorem
measure_theory.null_measurable_set_eq
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[measurable_singleton_class (measure_theory.null_measurable_space α μ)]
{a : α} :
measure_theory.null_measurable_set {x : α | x = a} μ
@[protected]
theorem
set.finite.null_measurable_set
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[measurable_singleton_class (measure_theory.null_measurable_space α μ)]
(hs : s.finite) :
@[protected]
theorem
finset.null_measurable_set
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[measurable_singleton_class (measure_theory.null_measurable_space α μ)]
(s : finset α) :
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_sUnion
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set (set α)}
(hs : s.finite)
(h : ∀ (t : set α), t ∈ s → measure_theory.null_measurable_set t μ) :
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) μ
theorem
set.finite.null_measurable_set_sInter
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set (set α)}
(hs : s.finite)
(h : ∀ (t : set α), t ∈ s → measure_theory.null_measurable_set t μ) :
theorem
measure_theory.null_measurable_set_to_measurable
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α} :
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
- measure_theory.null_measurable f μ = ∀ ⦃s : set β⦄, measurable_set s → measure_theory.null_measurable_set (f ⁻¹' s) μ
@[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.measurable'
{α : Type u_2}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
(h : measure_theory.null_measurable f μ) :
theorem
measure_theory.measurable.comp_null_measurable
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β}
{μ : measure_theory.measure α}
{g : β → γ}
(hg : measurable g)
(hf : measure_theory.null_measurable f μ) :
measure_theory.null_measurable (g ∘ f) μ
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.measure.is_complete_iff
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
μ.is_complete ↔ ∀ (s : set α), ⇑μ s = 0 → measurable_set s
theorem
measure_theory.measure.is_complete.out
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
(h : μ.is_complete)
(s : set α) :
⇑μ s = 0 → measurable_set s
theorem
measure_theory.measurable_set_of_null
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[μ.is_complete]
(hs : ⇑μ s = 0) :
theorem
measure_theory.null_measurable_set.measurable_of_complete
{α : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.null_measurable_set s μ)
[μ.is_complete] :
theorem
measure_theory.null_measurable.measurable_of_complete
{α : Type u_2}
{β : Type u_3}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[μ.is_complete]
{m1 : measurable_space β}
{f : α → β}
(hf : measure_theory.null_measurable f μ) :
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) :
def
measure_theory.measure.completion
{α : Type u_2}
{_x : measurable_space α}
(μ : measure_theory.measure α) :
Given a measure we can complete it to a (complete) measure on all null measurable sets.
Equations
- μ.completion = {to_outer_measure := μ.to_outer_measure, m_Union := _, trimmed := _}
Instances for measure_theory.measure.completion
@[protected, instance]
def
measure_theory.measure.completion.is_complete
{α : Type u_2}
{m : measurable_space α}
(μ : measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.coe_completion
{α : Type u_2}
{_x : measurable_space α}
(μ : measure_theory.measure α) :
⇑(μ.completion) = ⇑μ
theorem
measure_theory.measure.completion_apply
{α : Type u_2}
{_x : measurable_space α}
(μ : measure_theory.measure α)
(s : set α) :
⇑(μ.completion) s = ⇑μ s