Measurable spaces and measurable functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Do not add measurability lemmas (which could be tagged with
@[measurability]) to this file, since the measurability tactic is downstream
from here. Use measure_theory.measurable_space instead.
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
@[class]
- measurable_set' : set α → Prop
- measurable_set_empty : self.measurable_set' ∅
- measurable_set_compl : ∀ (s : set α), self.measurable_set' s → self.measurable_set' sᶜ
- measurable_set_Union : ∀ (f : ℕ → set α), (∀ (i : ℕ), self.measurable_set' (f i)) → self.measurable_set' (⋃ (i : ℕ), f i)
A measurable space is a space equipped with a σ-algebra.
Instances of this typeclass
- measure_theory.measure_space.to_measurable_space
- is_R_or_C.measurable_space
- order_dual.measurable_space
- empty.measurable_space
- punit.measurable_space
- bool.measurable_space
- Prop.measurable_space
- nat.measurable_space
- int.measurable_space
- rat.measurable_space
- quot.measurable_space
- quotient.measurable_space
- quotient_group.measurable_space
- quotient_add_group.measurable_space
- subtype.measurable_space
- prod.measurable_space
- measurable_space.pi
- tprod.measurable_space
- sum.measurable_space
- sigma.measurable_space
- measure_theory.null_measurable_space.measurable_space
- units.measurable_space
- add_units.measurable_space
- mul_opposite.measurable_space
- add_opposite.measurable_space
- real.measurable_space
- nnreal.measurable_space
- ennreal.measurable_space
- ereal.measurable_space
- complex.measurable_space
- measure_theory.measure.measurable_space
- euclidean_space.measurable_space
- continuous_linear_map.measurable_space
- add_circle.measurable_space
- Meas.measurable_space
- theorems_100.fin.measurable_space
Instances of other typeclasses for measurable_space
- measurable_space.has_sizeof_inst
- measurable_space.has_le
- measurable_space.partial_order
- measurable_space.complete_lattice
- measurable_space.inhabited
@[protected, instance]
Equations
measurable_set s means that s is measurable (in the ambient measure space on α)
Equations
- measurable_set = _inst_1.measurable_set'
@[simp, measurability]
@[measurability]
theorem
measurable_set.of_compl
{α : Type u_1}
{s : set α}
{m : measurable_space α}
(h : measurable_set sᶜ) :
@[simp]
@[simp, measurability]
@[measurability]
theorem
subsingleton.measurable_set
{α : Type u_1}
{m : measurable_space α}
[subsingleton α]
{s : set α} :
theorem
measurable_set.congr
{α : Type u_1}
{m : measurable_space α}
{s t : set α}
(hs : measurable_set s)
(h : s = t) :
theorem
measurable_set.bUnion_decode₂
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[encodable β]
⦃f : β → set α⦄
(h : ∀ (b : β), measurable_set (f b))
(n : ℕ) :
measurable_set (⋃ (b : β) (H : b ∈ encodable.decode₂ β n), f b)
@[measurability]
theorem
measurable_set.Union
{α : Type u_1}
{ι : Sort u_6}
{m : measurable_space α}
[countable ι]
⦃f : ι → set α⦄
(h : ∀ (b : ι), measurable_set (f b)) :
measurable_set (⋃ (b : ι), f b)
theorem
measurable_set.bUnion
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{f : β → set α}
{s : set β}
(hs : s.countable)
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
measurable_set (⋃ (b : β) (H : b ∈ s), f b)
theorem
set.finite.measurable_set_bUnion
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{f : β → set α}
{s : set β}
(hs : s.finite)
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
measurable_set (⋃ (b : β) (H : b ∈ s), f b)
theorem
finset.measurable_set_bUnion
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{f : β → set α}
(s : finset β)
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
measurable_set (⋃ (b : β) (H : b ∈ s), f b)
theorem
measurable_set.sUnion
{α : Type u_1}
{m : measurable_space α}
{s : set (set α)}
(hs : s.countable)
(h : ∀ (t : set α), t ∈ s → measurable_set t) :
measurable_set (⋃₀ s)
theorem
set.finite.measurable_set_sUnion
{α : Type u_1}
{m : measurable_space α}
{s : set (set α)}
(hs : s.finite)
(h : ∀ (t : set α), t ∈ s → measurable_set t) :
measurable_set (⋃₀ s)
@[measurability]
theorem
measurable_set.Inter
{α : Type u_1}
{ι : Sort u_6}
{m : measurable_space α}
[countable ι]
{f : ι → set α}
(h : ∀ (b : ι), measurable_set (f b)) :
measurable_set (⋂ (b : ι), f b)
theorem
measurable_set.bInter
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{f : β → set α}
{s : set β}
(hs : s.countable)
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
measurable_set (⋂ (b : β) (H : b ∈ s), f b)
theorem
set.finite.measurable_set_bInter
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{f : β → set α}
{s : set β}
(hs : s.finite)
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
measurable_set (⋂ (b : β) (H : b ∈ s), f b)
theorem
finset.measurable_set_bInter
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{f : β → set α}
(s : finset β)
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
measurable_set (⋂ (b : β) (H : b ∈ s), f b)
theorem
measurable_set.sInter
{α : Type u_1}
{m : measurable_space α}
{s : set (set α)}
(hs : s.countable)
(h : ∀ (t : set α), t ∈ s → measurable_set t) :
measurable_set (⋂₀ s)
theorem
set.finite.measurable_set_sInter
{α : Type u_1}
{m : measurable_space α}
{s : set (set α)}
(hs : s.finite)
(h : ∀ (t : set α), t ∈ s → measurable_set t) :
measurable_set (⋂₀ s)
@[simp, measurability]
theorem
measurable_set.union
{α : Type u_1}
{m : measurable_space α}
{s₁ s₂ : set α}
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂) :
measurable_set (s₁ ∪ s₂)
@[simp, measurability]
theorem
measurable_set.inter
{α : Type u_1}
{m : measurable_space α}
{s₁ s₂ : set α}
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂) :
measurable_set (s₁ ∩ s₂)
@[simp, measurability]
theorem
measurable_set.diff
{α : Type u_1}
{m : measurable_space α}
{s₁ s₂ : set α}
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂) :
measurable_set (s₁ \ s₂)
@[simp, measurability]
theorem
measurable_set.symm_diff
{α : Type u_1}
{m : measurable_space α}
{s₁ s₂ : set α}
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂) :
measurable_set (s₁ ∆ s₂)
@[simp, measurability]
theorem
measurable_set.ite
{α : Type u_1}
{m : measurable_space α}
{t s₁ s₂ : set α}
(ht : measurable_set t)
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂) :
measurable_set (t.ite s₁ s₂)
theorem
measurable_set.ite'
{α : Type u_1}
{m : measurable_space α}
{s t : set α}
{p : Prop}
(hs : p → measurable_set s)
(ht : ¬p → measurable_set t) :
measurable_set (ite p s t)
@[simp, measurability]
theorem
measurable_set.cond
{α : Type u_1}
{m : measurable_space α}
{s₁ s₂ : set α}
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂)
{i : bool} :
measurable_set (cond i s₁ s₂)
@[simp, measurability]
theorem
measurable_set.disjointed
{α : Type u_1}
{m : measurable_space α}
{f : ℕ → set α}
(h : ∀ (i : ℕ), measurable_set (f i))
(n : ℕ) :
measurable_set (disjointed f n)
@[measurability]
theorem
measurable_set.const
{α : Type u_1}
{m : measurable_space α}
(p : Prop) :
measurable_set {a : α | p}
theorem
nonempty_measurable_superset
{α : Type u_1}
{m : measurable_space α}
(s : set α) :
nonempty {t // s ⊆ t ∧ measurable_set t}
Every set has a measurable superset. Declare this as local instance as needed.
@[ext]
theorem
measurable_space.ext
{α : Type u_1}
{m₁ m₂ : measurable_space α} :
(∀ (s : set α), measurable_set s ↔ measurable_set s) → m₁ = m₂
@[ext]
theorem
measurable_space.ext_iff
{α : Type u_1}
{m₁ m₂ : measurable_space α} :
m₁ = m₂ ↔ ∀ (s : set α), measurable_set s ↔ measurable_set s
@[class]
- measurable_set_singleton : ∀ (x : α), measurable_set {x}
A typeclass mixin for measurable_spaces such that each singleton is measurable.
Instances of this typeclass
- measurable_space.top.measurable_singleton_class
- opens_measurable_space.to_measurable_singleton_class
- empty.measurable_singleton_class
- punit.measurable_singleton_class
- bool.measurable_singleton_class
- Prop.measurable_singleton_class
- nat.measurable_singleton_class
- int.measurable_singleton_class
- rat.measurable_singleton_class
- subtype.measurable_singleton_class
- prod.measurable_singleton_class
- pi.measurable_singleton_class
- measure_theory.null_measurable_set.measure_theory.null_measurable_space.measurable_singleton_class
- theorems_100.fin.measurable_singleton_class
@[measurability]
theorem
measurable_set_eq
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{a : α} :
measurable_set {x : α | x = a}
@[measurability]
theorem
measurable_set.insert
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{s : set α}
(hs : measurable_set s)
(a : α) :
@[simp]
theorem
measurable_set_insert
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{a : α}
{s : set α} :
theorem
set.subsingleton.measurable_set
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{s : set α}
(hs : s.subsingleton) :
theorem
set.finite.measurable_set
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{s : set α}
(hs : s.finite) :
@[protected, measurability]
theorem
finset.measurable_set
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(s : finset α) :
theorem
set.countable.measurable_set
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{s : set α}
(hs : s.countable) :
@[protected, instance]
Equations
- measurable_space.has_le = {le := λ (m₁ m₂ : measurable_space α), ∀ (s : set α), measurable_set s → measurable_set s}
theorem
measurable_space.le_def
{α : Type u_1}
{a b : measurable_space α} :
a ≤ b ↔ a.measurable_set' ≤ b.measurable_set'
@[protected, instance]
Equations
- measurable_space.partial_order = {le := has_le.le measurable_space.has_le, lt := λ (m₁ m₂ : measurable_space α), m₁ ≤ m₂ ∧ ¬m₂ ≤ m₁, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
- basic : ∀ {α : Type u_1} {s : set (set α)} (u : set α), u ∈ s → measurable_space.generate_measurable s u
- empty : ∀ {α : Type u_1} {s : set (set α)}, measurable_space.generate_measurable s ∅
- compl : ∀ {α : Type u_1} {s : set (set α)} (s_1 : set α), measurable_space.generate_measurable s s_1 → measurable_space.generate_measurable s s_1ᶜ
- union : ∀ {α : Type u_1} {s : set (set α)} (f : ℕ → set α), (∀ (n : ℕ), measurable_space.generate_measurable s (f n)) → measurable_space.generate_measurable s (⋃ (i : ℕ), f i)
The smallest σ-algebra containing a collection s of basic sets
Construct the smallest measure space containing a collection of basic sets
Equations
theorem
measurable_space.generate_from_induction
{α : Type u_1}
(p : set α → Prop)
(C : set (set α))
(hC : ∀ (t : set α), t ∈ C → p t)
(h_empty : p ∅)
(h_compl : ∀ (t : set α), p t → p tᶜ)
(h_Union : ∀ (f : ℕ → set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i))
{s : set α}
(hs : measurable_set s) :
p s
theorem
measurable_space.generate_from_le
{α : Type u_1}
{s : set (set α)}
{m : measurable_space α}
(h : ∀ (t : set α), t ∈ s → measurable_set t) :
theorem
measurable_space.generate_from_le_iff
{α : Type u_1}
{s : set (set α)}
(m : measurable_space α) :
measurable_space.generate_from s ≤ m ↔ s ⊆ {t : set α | measurable_set t}
@[simp]
theorem
measurable_space.generate_from_measurable_set
{α : Type u_1}
[measurable_space α] :
measurable_space.generate_from {s : set α | measurable_set s} = _inst_1
@[protected]
def
measurable_space.mk_of_closure
{α : Type u_1}
(g : set (set α))
(hg : {t : set α | measurable_set 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
- measurable_space.mk_of_closure g hg = {measurable_set' := λ (s : set α), s ∈ g, measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}
theorem
measurable_space.mk_of_closure_sets
{α : Type u_1}
{s : set (set α)}
{hs : {t : set α | measurable_set t} = s} :
def
measurable_space.gi_generate_from
{α : Type u_1} :
galois_insertion measurable_space.generate_from (λ (m : measurable_space α), {t : set α | measurable_set 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
- measurable_space.gi_generate_from = {choice := λ (g : set (set α)) (hg : {t : set α | measurable_set t} ≤ g), measurable_space.mk_of_closure g _, gc := _, le_l_u := _, choice_eq := _}
@[protected, instance]
@[protected, instance]
Equations
@[simp]
@[simp]
@[simp, measurability]
@[simp]
theorem
measurable_space.measurable_set_inf
{α : Type u_1}
{m₁ m₂ : measurable_space α}
{s : set α} :
@[simp]
theorem
measurable_space.measurable_set_Inf
{α : Type u_1}
{ms : set (measurable_space α)}
{s : set α} :
measurable_set s ↔ ∀ (m : measurable_space α), m ∈ ms → measurable_set s
@[simp]
theorem
measurable_space.measurable_set_infi
{α : Type u_1}
{ι : Sort u_2}
{m : ι → measurable_space α}
{s : set α} :
measurable_set s ↔ ∀ (i : ι), measurable_set s
theorem
measurable_space.measurable_set_sup
{α : Type u_1}
{m₁ m₂ : measurable_space α}
{s : set α} :
theorem
measurable_space.measurable_set_Sup
{α : Type u_1}
{ms : set (measurable_space α)}
{s : set α} :
measurable_set s ↔ measurable_space.generate_measurable {s : set α | ∃ (m : measurable_space α) (H : m ∈ ms), measurable_set s} s
theorem
measurable_space.measurable_set_supr
{α : Type u_1}
{ι : Sort u_2}
{m : ι → measurable_space α}
{s : set α} :
measurable_set s ↔ measurable_space.generate_measurable {s : set α | ∃ (i : ι), measurable_set s} s
theorem
measurable_space.measurable_space_supr_eq
{α : Type u_1}
{ι : Sort u_6}
(m : ι → measurable_space α) :
(⨆ (n : ι), m n) = measurable_space.generate_from {s : set α | ∃ (n : ι), measurable_set s}
theorem
measurable_space.generate_from_Union_measurable_set
{α : Type u_1}
{ι : Sort u_6}
(m : ι → measurable_space α) :
measurable_space.generate_from (⋃ (n : ι), {t : set α | measurable_set t}) = ⨆ (n : ι), m n
def
measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → β) :
Prop
A function f between measurable spaces is measurable if the preimage of every
measurable set is measurable.
Equations
- measurable f = ∀ ⦃t : set β⦄, measurable_set t → measurable_set (f ⁻¹' t)
Instances for measurable
@[measurability]
@[measurability]
theorem
measurable.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{g : β → γ}
{f : α → β}
(hg : measurable g)
(hf : measurable f) :
measurable (g ∘ f)
@[simp, measurability]
theorem
measurable_const
{α : Type u_1}
{β : Type u_2}
{ma : measurable_space α}
{mb : measurable_space β}
{a : α} :
measurable (λ (b : β), a)
theorem
measurable.le
{β : Type u_2}
{α : Type u_1}
{m m0 : measurable_space α}
{mb : measurable_space β}
(hm : m ≤ m0)
{f : α → β}
(hf : measurable f) :
theorem
measurable_space.top.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space β]
(f : α → β) :