Measurable spaces and measurable functions #
This file defines measurable spaces and measurable functions.
A measurable space is a set equipped with a σ-algebra, a collection of subsets closed under complementation and countable union. A function between measurable spaces is measurable if the preimage of each measurable subset is measurable.
σ-algebras on a fixed set α form a complete lattice. Here we order
σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is
also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any
collection of subsets of α generates a smallest σ-algebra which
contains all of them.
References #
- https://en.wikipedia.org/wiki/Measurable_space
- https://en.wikipedia.org/wiki/Sigma-algebra
- https://en.wikipedia.org/wiki/Dynkin_system
Tags #
measurable space, σ-algebra, measurable function
A measurable space is a space equipped with a σ-algebra.
Predicate saying that a given set is measurable. Use
MeasurableSetin the root namespace instead.- measurableSet_empty : MeasurableSet' self ∅
The empty set is a measurable set. Use
MeasurableSet.emptyinstead. - measurableSet_compl (s : Set α) : MeasurableSet' self s → MeasurableSet' self sᶜ
The complement of a measurable set is a measurable set. Use
MeasurableSet.complinstead. - measurableSet_iUnion (f : ℕ → Set α) : (∀ (i : ℕ), MeasurableSet' self (f i)) → MeasurableSet' self (⋃ (i : ℕ), f i)
The union of a sequence of measurable sets is a measurable set. Use a more general
MeasurableSet.iUnioninstead.
Instances
Equations
MeasurableSet s means that s is measurable (in the ambient measure space on α)
Equations
- MeasurableSet s = MeasurableSpace.MeasurableSet' inst✝ s
Instances For
Notation for MeasurableSet with respect to a non-standard σ-algebra.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasurableSet.compl
{α : Type u_1}
{s : Set α}
{m : MeasurableSpace α}
:
MeasurableSet s → MeasurableSet sᶜ
theorem
MeasurableSet.of_compl
{α : Type u_1}
{s : Set α}
{m : MeasurableSpace α}
(h : MeasurableSet sᶜ)
:
@[simp]
@[simp]
theorem
Subsingleton.measurableSet
{α : Type u_1}
{m : MeasurableSpace α}
[Subsingleton α]
{s : Set α}
:
theorem
MeasurableSet.congr
{α : Type u_1}
{m : MeasurableSpace α}
{s t : Set α}
(hs : MeasurableSet s)
(h : s = t)
:
theorem
MeasurableSet.iUnion
{α : Type u_1}
{ι : Sort u_6}
{m : MeasurableSpace α}
[Countable ι]
⦃f : ι → Set α⦄
(h : ∀ (b : ι), MeasurableSet (f b))
:
MeasurableSet (⋃ (b : ι), f b)
theorem
MeasurableSet.biUnion
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{f : β → Set α}
{s : Set β}
(hs : s.Countable)
(h : ∀ b ∈ s, MeasurableSet (f b))
:
MeasurableSet (⋃ b ∈ s, f b)
theorem
Set.Finite.measurableSet_biUnion
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{f : β → Set α}
{s : Set β}
(hs : s.Finite)
(h : ∀ b ∈ s, MeasurableSet (f b))
:
MeasurableSet (⋃ b ∈ s, f b)
theorem
Finset.measurableSet_biUnion
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{f : β → Set α}
(s : Finset β)
(h : ∀ b ∈ s, MeasurableSet (f b))
:
MeasurableSet (⋃ b ∈ s, f b)
theorem
MeasurableSet.sUnion
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set (Set α)}
(hs : s.Countable)
(h : ∀ t ∈ s, MeasurableSet t)
:
MeasurableSet (⋃₀ s)
theorem
Set.Finite.measurableSet_sUnion
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set (Set α)}
(hs : s.Finite)
(h : ∀ t ∈ s, MeasurableSet t)
:
MeasurableSet (⋃₀ s)
theorem
MeasurableSet.iInter
{α : Type u_1}
{ι : Sort u_6}
{m : MeasurableSpace α}
[Countable ι]
{f : ι → Set α}
(h : ∀ (b : ι), MeasurableSet (f b))
:
MeasurableSet (⋂ (b : ι), f b)
theorem
MeasurableSet.biInter
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{f : β → Set α}
{s : Set β}
(hs : s.Countable)
(h : ∀ b ∈ s, MeasurableSet (f b))
:
MeasurableSet (⋂ b ∈ s, f b)
theorem
Set.Finite.measurableSet_biInter
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{f : β → Set α}
{s : Set β}
(hs : s.Finite)
(h : ∀ b ∈ s, MeasurableSet (f b))
:
MeasurableSet (⋂ b ∈ s, f b)
theorem
Finset.measurableSet_biInter
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{f : β → Set α}
(s : Finset β)
(h : ∀ b ∈ s, MeasurableSet (f b))
:
MeasurableSet (⋂ b ∈ s, f b)
theorem
MeasurableSet.sInter
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set (Set α)}
(hs : s.Countable)
(h : ∀ t ∈ s, MeasurableSet t)
:
MeasurableSet (⋂₀ s)
theorem
Set.Finite.measurableSet_sInter
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set (Set α)}
(hs : s.Finite)
(h : ∀ t ∈ s, MeasurableSet t)
:
MeasurableSet (⋂₀ s)
@[simp]
theorem
MeasurableSet.union
{α : Type u_1}
{m : MeasurableSpace α}
{s₁ s₂ : Set α}
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
:
MeasurableSet (s₁ ∪ s₂)
@[simp]
theorem
MeasurableSet.inter
{α : Type u_1}
{m : MeasurableSpace α}
{s₁ s₂ : Set α}
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
:
MeasurableSet (s₁ ∩ s₂)
@[simp]
theorem
MeasurableSet.diff
{α : Type u_1}
{m : MeasurableSpace α}
{s₁ s₂ : Set α}
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
:
MeasurableSet (s₁ \ s₂)
@[simp]
theorem
MeasurableSet.himp
{α : Type u_1}
{m : MeasurableSpace α}
{s₁ s₂ : Set α}
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
:
MeasurableSet (s₁ ⇨ s₂)
@[simp]
theorem
MeasurableSet.symmDiff
{α : Type u_1}
{m : MeasurableSpace α}
{s₁ s₂ : Set α}
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
:
MeasurableSet (symmDiff s₁ s₂)
@[simp]
theorem
MeasurableSet.bihimp
{α : Type u_1}
{m : MeasurableSpace α}
{s₁ s₂ : Set α}
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
:
MeasurableSet (bihimp s₁ s₂)
@[simp]
theorem
MeasurableSet.ite
{α : Type u_1}
{m : MeasurableSpace α}
{t s₁ s₂ : Set α}
(ht : MeasurableSet t)
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
:
MeasurableSet (t.ite s₁ s₂)
theorem
MeasurableSet.ite'
{α : Type u_1}
{m : MeasurableSpace α}
{s t : Set α}
{p : Prop}
(hs : p → MeasurableSet s)
(ht : ¬p → MeasurableSet t)
:
MeasurableSet (if p then s else t)
@[simp]
theorem
MeasurableSet.cond
{α : Type u_1}
{m : MeasurableSpace α}
{s₁ s₂ : Set α}
(h₁ : MeasurableSet s₁)
(h₂ : MeasurableSet s₂)
{i : Bool}
:
MeasurableSet (bif i then s₁ else s₂)
theorem
MeasurableSet.const
{α : Type u_1}
{m : MeasurableSpace α}
(p : Prop)
:
MeasurableSet {_a : α | p}
Every set has a measurable superset. Declare this as local instance as needed.
theorem
MeasurableSpace.ext
{α : Type u_1}
{m₁ m₂ : MeasurableSpace α}
(h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s)
:
A typeclass mixin for MeasurableSpaces such that each singleton is measurable.
- measurableSet_singleton (x : α) : MeasurableSet {x}
A singleton is a measurable set.
Instances
@[simp]
theorem
MeasurableSet.singleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(a : α)
:
theorem
MeasurableSet.insert
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
{s : Set α}
(hs : MeasurableSet s)
(a : α)
:
MeasurableSet (insert a s)
@[simp]
theorem
measurableSet_insert
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
{a : α}
{s : Set α}
:
theorem
Set.Subsingleton.measurableSet
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
{s : Set α}
(hs : s.Subsingleton)
:
theorem
Set.Finite.measurableSet
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
{s : Set α}
(hs : s.Finite)
:
theorem
Finset.measurableSet
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(s : Finset α)
:
theorem
Set.Countable.measurableSet
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
{s : Set α}
(hs : s.Countable)
:
def
MeasurableSpace.copy
{α : Type u_1}
(m : MeasurableSpace α)
(p : Set α → Prop)
(h : ∀ (s : Set α), p s ↔ MeasurableSet s)
:
Copy of a MeasurableSpace with a new MeasurableSet equal to the old one. Useful to fix
definitional equalities.
Equations
Instances For
theorem
MeasurableSpace.measurableSet_copy
{α : Type u_1}
{m : MeasurableSpace α}
{p : Set α → Prop}
(h : ∀ (s : Set α), p s ↔ MeasurableSet s)
{s : Set α}
:
theorem
MeasurableSpace.copy_eq
{α : Type u_1}
{m : MeasurableSpace α}
{p : Set α → Prop}
(h : ∀ (s : Set α), p s ↔ MeasurableSet s)
:
Equations
- MeasurableSpace.instLE = { le := fun (m₁ m₂ : MeasurableSpace α) => ∀ (s : Set α), MeasurableSet s → MeasurableSet s }
Equations
- One or more equations did not get rendered due to their size.
The smallest σ-algebra containing a collection s of basic sets
- basic {α : Type u_1} {s : Set (Set α)} (u : Set α) : u ∈ s → GenerateMeasurable s u
- empty {α : Type u_1} {s : Set (Set α)} : GenerateMeasurable s ∅
- compl {α : Type u_1} {s : Set (Set α)} (t : Set α) : GenerateMeasurable s t → GenerateMeasurable s tᶜ
- iUnion {α : Type u_1} {s : Set (Set α)} (f : ℕ → Set α) : (∀ (n : ℕ), GenerateMeasurable s (f n)) → GenerateMeasurable s (⋃ (i : ℕ), f i)
Instances For
Construct the smallest measure space containing a collection of basic sets
Equations
- MeasurableSpace.generateFrom s = { MeasurableSet' := MeasurableSpace.GenerateMeasurable s, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }
Instances For
theorem
MeasurableSpace.generateFrom_induction
{α : Type u_1}
(C : Set (Set α))
(p : (s : Set α) → MeasurableSet s → Prop)
(hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht)
(empty : p ∅ ⋯)
(compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯)
(iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯)
(s : Set α)
(hs : MeasurableSet s)
:
p s hs
theorem
MeasurableSpace.generateFrom_le
{α : Type u_1}
{s : Set (Set α)}
{m : MeasurableSpace α}
(h : ∀ t ∈ s, MeasurableSet t)
:
theorem
MeasurableSpace.generateFrom_le_iff
{α : Type u_1}
{s : Set (Set α)}
(m : MeasurableSpace α)
:
@[simp]
def
MeasurableSpace.mkOfClosure
{α : Type u_1}
(g : Set (Set α))
(hg : {t : Set α | MeasurableSet t} = g)
:
If g is a collection of subsets of α such that the σ-algebra generated from g contains
the same sets as g, then g was already a σ-algebra.
Equations
- MeasurableSpace.mkOfClosure g hg = (MeasurableSpace.generateFrom g).copy (fun (x : Set α) => x ∈ g) ⋯
Instances For
def
MeasurableSpace.giGenerateFrom
{α : Type u_1}
:
GaloisInsertion generateFrom fun (m : MeasurableSpace α) => {t : Set α | MeasurableSet t}
We get a Galois insertion between σ-algebras on α and Set (Set α) by using generate_from
on one side and the collection of measurable sets on the other side.
Equations
- MeasurableSpace.giGenerateFrom = { choice := fun (g : Set (Set α)) (hg : {t : Set α | MeasurableSet t} ≤ g) => MeasurableSpace.mkOfClosure g ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Equations
- MeasurableSpace.instInhabited = { default := ⊤ }
@[simp]
@[simp]
@[simp]
@[simp]
theorem
MeasurableSpace.measurableSet_sInf
{α : Type u_1}
{ms : Set (MeasurableSpace α)}
{s : Set α}
:
theorem
MeasurableSpace.measurableSet_iInf
{α : Type u_1}
{ι : Sort u_7}
{m : ι → MeasurableSpace α}
{s : Set α}
:
theorem
MeasurableSpace.measurableSet_sSup
{α : Type u_1}
{ms : Set (MeasurableSpace α)}
{s : Set α}
:
theorem
MeasurableSpace.measurableSet_iSup
{α : Type u_1}
{ι : Sort u_7}
{m : ι → MeasurableSpace α}
{s : Set α}
:
theorem
MeasurableSpace.measurableSpace_iSup_eq
{α : Type u_1}
{ι : Sort u_6}
(m : ι → MeasurableSpace α)
:
theorem
MeasurableSpace.generateFrom_iUnion_measurableSet
{α : Type u_1}
{ι : Sort u_6}
(m : ι → MeasurableSpace α)
:
A function f between measurable spaces is measurable if the preimage of every
measurable set is measurable.
Equations
- Measurable f = ∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (f ⁻¹' t)
Instances For
Notation for Measurable with respect to a non-standard σ-algebra in the domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for Measurable with respect to a non-standard σ-algebra in the domain and codomain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Measurable.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace γ}
{g : β → γ}
{f : α → β}
(hg : Measurable g)
(hf : Measurable f)
:
Measurable (g ∘ f)
theorem
Measurable.comp'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{x✝² : MeasurableSpace γ}
{g : β → γ}
{f : α → β}
(hg : Measurable g)
(hf : Measurable f)
:
Measurable fun (x : α) => g (f x)
@[simp]
theorem
measurable_const
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{a : α}
:
Measurable fun (x : β) => a
theorem
Measurable.le
{β : Type u_2}
{α : Type u_7}
{m m0 : MeasurableSpace α}
{x✝ : MeasurableSpace β}
(hm : m ≤ m0)
{f : α → β}
(hf : Measurable f)
:
A typeclass mixin for MeasurableSpaces such that all sets are measurable.
- forall_measurableSet (s : Set α) : MeasurableSet s
Do not use this. Use
MeasurableSet.of_discreteinstead.
Instances
@[instance 100]
instance
MeasurableSingletonClass.toDiscreteMeasurableSpace
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Countable α]
:
theorem
MeasurableSet.of_discrete
{α : Type u_1}
[MeasurableSpace α]
[DiscreteMeasurableSpace α]
{s : Set α}
:
theorem
Measurable.of_discrete
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[DiscreteMeasurableSpace α]
{f : α → β}
:
@[instance 100]
instance
DiscreteMeasurableSpace.toMeasurableSingletonClass
{α : Type u_1}
[MeasurableSpace α]
[DiscreteMeasurableSpace α]
:
Warning: Creates a typeclass loop with MeasurableSingletonClass.toDiscreteMeasurableSpace.
To be monitored.