Measurable spaces and measurable functions
This file defines measurable spaces and the functions and isomorphisms between them.
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. A function f : α → β induces a Galois connection
between the lattices of σ-algebras on α and β.
A measurable equivalence between measurable spaces is an equivalence which respects the σ-algebras, that is, for which both directions of the equivalence are measurable functions.
We say that a filter f is measurably generated if every set s ∈ f includes a measurable
set t ∈ f. This property is useful, e.g., to extract a measurable witness of filter.eventually.
Main statements
The main theorem of this file is Dynkin's π-λ theorem, which appears
here as an induction principle induction_on_inter. Suppose s is a
collection of subsets of α such that the intersection of two members
of s belongs to s whenever it is nonempty. Let m be the σ-algebra
generated by s. In order to check that a predicate C holds on every
member of m, it suffices to check that C holds on the members of s and
that C is preserved by complementation and disjoint countable
unions.
Implementation notes
Measurability of a function f : α → β between measurable spaces is
defined in terms of the Galois connection induced by f.
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, measurable function, dynkin system
@[class]
- is_measurable' : set α → Prop
- is_measurable_empty : c.is_measurable' ∅
- is_measurable_compl : ∀ (s : set α), c.is_measurable' s → c.is_measurable' sᶜ
- is_measurable_Union : ∀ (f : ℕ → set α), (∀ (i : ℕ), c.is_measurable' (f i)) → c.is_measurable' (⋃ (i : ℕ), f i)
A measurable space is a space equipped with a σ-algebra.
Instances
- measure_theory.measure_space.to_measurable_space
- empty.measurable_space
- unit.measurable_space
- bool.measurable_space
- nat.measurable_space
- int.measurable_space
- rat.measurable_space
- subtype.measurable_space
- prod.measurable_space
- measurable_space.pi
- sum.measurable_space
- sigma.measurable_space
- real.measurable_space
- nnreal.measurable_space
- ennreal.measurable_space
- complex.measurable_space
- measure_theory.measure.measurable_space
- Meas.measurable_space
is_measurable s means that s is measurable (in the ambient measure space on α)
Equations
- is_measurable = _inst_1.is_measurable'
theorem
is_measurable.of_compl
{α : Type u}
{s : set α}
[measurable_space α]
(h : is_measurable sᶜ) :
@[simp]
@[simp]
theorem
is_measurable.congr
{α : Type u}
[measurable_space α]
{s t : set α}
(hs : is_measurable s)
(h : s = t) :
theorem
is_measurable.bUnion_decode2
{α : Type u}
{β : Type v}
[measurable_space α]
[encodable β]
⦃f : β → set α⦄
(h : ∀ (b : β), is_measurable (f b))
(n : ℕ) :
is_measurable (⋃ (b : β) (H : b ∈ encodable.decode2 β n), f b)
theorem
is_measurable.Union
{α : Type u}
{β : Type v}
[measurable_space α]
[encodable β]
⦃f : β → set α⦄
(h : ∀ (b : β), is_measurable (f b)) :
is_measurable (⋃ (b : β), f b)
theorem
is_measurable.bUnion
{α : Type u}
{β : Type v}
[measurable_space α]
{f : β → set α}
{s : set β}
(hs : s.countable)
(h : ∀ (b : β), b ∈ s → is_measurable (f b)) :
is_measurable (⋃ (b : β) (H : b ∈ s), f b)
theorem
is_measurable.sUnion
{α : Type u}
[measurable_space α]
{s : set (set α)}
(hs : s.countable)
(h : ∀ (t : set α), t ∈ s → is_measurable t) :
is_measurable (⋃₀s)
theorem
is_measurable.Union_Prop
{α : Type u}
[measurable_space α]
{p : Prop}
{f : p → set α}
(hf : ∀ (b : p), is_measurable (f b)) :
is_measurable (⋃ (b : p), f b)
theorem
is_measurable.Inter
{α : Type u}
{β : Type v}
[measurable_space α]
[encodable β]
{f : β → set α}
(h : ∀ (b : β), is_measurable (f b)) :
is_measurable (⋂ (b : β), f b)
theorem
is_measurable.bInter
{α : Type u}
{β : Type v}
[measurable_space α]
{f : β → set α}
{s : set β}
(hs : s.countable)
(h : ∀ (b : β), b ∈ s → is_measurable (f b)) :
is_measurable (⋂ (b : β) (H : b ∈ s), f b)
theorem
is_measurable.sInter
{α : Type u}
[measurable_space α]
{s : set (set α)}
(hs : s.countable)
(h : ∀ (t : set α), t ∈ s → is_measurable t) :
is_measurable (⋂₀s)
theorem
is_measurable.Inter_Prop
{α : Type u}
[measurable_space α]
{p : Prop}
{f : p → set α}
(hf : ∀ (b : p), is_measurable (f b)) :
is_measurable (⋂ (b : p), f b)
@[simp]
theorem
is_measurable.union
{α : Type u}
[measurable_space α]
{s₁ s₂ : set α}
(h₁ : is_measurable s₁)
(h₂ : is_measurable s₂) :
is_measurable (s₁ ∪ s₂)
@[simp]
theorem
is_measurable.inter
{α : Type u}
[measurable_space α]
{s₁ s₂ : set α}
(h₁ : is_measurable s₁)
(h₂ : is_measurable s₂) :
is_measurable (s₁ ∩ s₂)
@[simp]
theorem
is_measurable.diff
{α : Type u}
[measurable_space α]
{s₁ s₂ : set α}
(h₁ : is_measurable s₁)
(h₂ : is_measurable s₂) :
is_measurable (s₁ \ s₂)
@[simp]
theorem
is_measurable.disjointed
{α : Type u}
[measurable_space α]
{f : ℕ → set α}
(h : ∀ (i : ℕ), is_measurable (f i))
(n : ℕ) :
is_measurable (set.disjointed f n)
@[simp]
theorem
is_measurable.const
{α : Type u}
[measurable_space α]
(p : Prop) :
is_measurable {a : α | p}
@[ext]
theorem
measurable_space.ext
{α : Type u}
{m₁ m₂ : measurable_space α}
(a : ∀ (s : set α), m₁.is_measurable' s ↔ m₂.is_measurable' s) :
m₁ = m₂
@[ext]
theorem
measurable_space.ext_iff
{α : Type u}
{m₁ m₂ : measurable_space α} :
m₁ = m₂ ↔ ∀ (s : set α), m₁.is_measurable' s ↔ m₂.is_measurable' s
@[class]
- is_measurable_singleton : ∀ (x : α), is_measurable {x}
A typeclass mixin for measurable_spaces such that each singleton is measurable.
theorem
is_measurable_eq
{α : Type u}
[measurable_space α]
[measurable_singleton_class α]
{a : α} :
is_measurable {x : α | x = a}
theorem
is_measurable.insert
{α : Type u}
[measurable_space α]
[measurable_singleton_class α]
{s : set α}
(hs : is_measurable s)
(a : α) :
is_measurable (insert a s)
@[simp]
theorem
is_measurable_insert
{α : Type u}
[measurable_space α]
[measurable_singleton_class α]
{a : α}
{s : set α} :
is_measurable (insert a s) ↔ is_measurable s
theorem
set.finite.is_measurable
{α : Type u}
[measurable_space α]
[measurable_singleton_class α]
{s : set α}
(hs : s.finite) :
theorem
finset.is_measurable
{α : Type u}
[measurable_space α]
[measurable_singleton_class α]
(s : finset α) :
@[instance]
Equations
- measurable_space.partial_order = {le := λ (m₁ m₂ : measurable_space α), m₁.is_measurable' ≤ m₂.is_measurable', lt := preorder.lt._default (λ (m₁ m₂ : measurable_space α), m₁.is_measurable' ≤ m₂.is_measurable'), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
- basic : ∀ {α : Type u} (s : set (set α)) (u : set α), u ∈ s → measurable_space.generate_measurable s u
- empty : ∀ {α : Type u} (s : set (set α)), measurable_space.generate_measurable s ∅
- compl : ∀ {α : Type u} (s : set (set α)) (s_1 : set α), measurable_space.generate_measurable s s_1 → measurable_space.generate_measurable s s_1ᶜ
- union : ∀ {α : Type u} (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.is_measurable_generate_from
{α : Type u}
{s : set (set α)}
{t : set α}
(ht : t ∈ s) :
theorem
measurable_space.generate_from_le
{α : Type u}
{s : set (set α)}
{m : measurable_space α}
(h : ∀ (t : set α), t ∈ s → m.is_measurable' t) :
theorem
measurable_space.generate_from_le_iff
{α : Type u}
{s : set (set α)}
(m : measurable_space α) :
measurable_space.generate_from s ≤ m ↔ s ⊆ {t : set α | m.is_measurable' t}
def
measurable_space.mk_of_closure
{α : Type u}
(g : set (set α))
(hg : {t : set α | (measurable_space.generate_from g).is_measurable' 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 = {is_measurable' := λ (s : set α), s ∈ g, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}
theorem
measurable_space.mk_of_closure_sets
{α : Type u}
{s : set (set α)}
{hs : {t : set α | (measurable_space.generate_from s).is_measurable' t} = s} :
def
measurable_space.gi_generate_from
{α : Type u} :
galois_insertion measurable_space.generate_from (λ (m : measurable_space α), {t : set α | is_measurable 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 α | is_measurable t} ≤ g), measurable_space.mk_of_closure g _, gc := _, le_l_u := _, choice_eq := _}
@[instance]
@[instance]
Equations
@[simp]
@[simp]
@[simp]
theorem
measurable_space.is_measurable_Inf
{α : Type u}
{ms : set (measurable_space α)}
{s : set α} :
is_measurable s ↔ ∀ (m : measurable_space α), m ∈ ms → is_measurable s
@[simp]
theorem
measurable_space.is_measurable_infi
{α : Type u}
{ι : Sort u_1}
{m : ι → measurable_space α}
{s : set α} :
is_measurable s ↔ ∀ (i : ι), is_measurable s
theorem
measurable_space.is_measurable_Sup
{α : Type u}
{ms : set (measurable_space α)}
{s : set α} :
theorem
measurable_space.is_measurable_supr
{α : Type u}
{ι : Sort u_1}
{m : ι → measurable_space α}
{s : set α} :
is_measurable s ↔ measurable_space.generate_measurable (⋃ (i : ι), (m i).is_measurable') s
The forward image of a measure space under a function. map f m contains the sets s : set β
whose preimage under f is measurable.
Equations
- measurable_space.map f m = {is_measurable' := λ (s : set β), m.is_measurable' (f ⁻¹' s), is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}
@[simp]
theorem
measurable_space.map_id
{α : Type u}
{m : measurable_space α} :
measurable_space.map id m = m
@[simp]
theorem
measurable_space.map_comp
{α : Type u}
{β : Type v}
{γ : Type w}
{m : measurable_space α}
{f : α → β}
{g : β → γ} :
measurable_space.map g (measurable_space.map f m) = measurable_space.map (g ∘ f) m
The reverse image of a measure space under a function. comap f m contains the sets s : set α
such that s is the f-preimage of a measurable set in β.
Equations
- measurable_space.comap f m = {is_measurable' := λ (s : set α), ∃ (s' : set β), m.is_measurable' s' ∧ f ⁻¹' s' = s, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}
@[simp]
@[simp]
theorem
measurable_space.comap_comp
{α : Type u}
{β : Type v}
{γ : Type w}
{m : measurable_space α}
{f : β → α}
{g : γ → β} :
measurable_space.comap g (measurable_space.comap f m) = measurable_space.comap (f ∘ g) m
theorem
measurable_space.comap_le_iff_le_map
{α : Type u}
{β : Type v}
{m : measurable_space α}
{m' : measurable_space β}
{f : α → β} :
measurable_space.comap f m' ≤ m ↔ m' ≤ measurable_space.map f m
theorem
measurable_space.map_mono
{α : Type u}
{β : Type v}
{m₁ m₂ : measurable_space α}
{f : α → β}
(h : m₁ ≤ m₂) :
measurable_space.map f m₁ ≤ measurable_space.map f m₂
theorem
measurable_space.comap_mono
{α : Type u}
{β : Type v}
{m₁ m₂ : measurable_space α}
{g : β → α}
(h : m₁ ≤ m₂) :
measurable_space.comap g m₁ ≤ measurable_space.comap g m₂
@[simp]
@[simp]
theorem
measurable_space.comap_sup
{α : Type u}
{β : Type v}
{m₁ m₂ : measurable_space α}
{g : β → α} :
measurable_space.comap g (m₁ ⊔ m₂) = measurable_space.comap g m₁ ⊔ measurable_space.comap g m₂
@[simp]
theorem
measurable_space.comap_supr
{α : Type u}
{β : Type v}
{ι : Sort x}
{g : β → α}
{m : ι → measurable_space α} :
measurable_space.comap g (⨆ (i : ι), m i) = ⨆ (i : ι), measurable_space.comap g (m i)
@[simp]
@[simp]
theorem
measurable_space.map_inf
{α : Type u}
{β : Type v}
{m₁ m₂ : measurable_space α}
{f : α → β} :
measurable_space.map f (m₁ ⊓ m₂) = measurable_space.map f m₁ ⊓ measurable_space.map f m₂
@[simp]
theorem
measurable_space.map_infi
{α : Type u}
{β : Type v}
{ι : Sort x}
{f : α → β}
{m : ι → measurable_space α} :
measurable_space.map f (⨅ (i : ι), m i) = ⨅ (i : ι), measurable_space.map f (m i)
theorem
measurable_space.comap_map_le
{α : Type u}
{β : Type v}
{m : measurable_space α}
{f : α → β} :
measurable_space.comap f (measurable_space.map f m) ≤ m
theorem
measurable_space.le_map_comap
{α : Type u}
{β : Type v}
{m : measurable_space α}
{g : β → α} :
m ≤ measurable_space.map g (measurable_space.comap g m)
theorem
measurable_space.generate_from_le_generate_from
{α : Type u}
{s t : set (set α)}
(h : s ⊆ t) :
theorem
measurable_space.comap_generate_from
{α : Type u}
{β : Type v}
{f : α → β}
{s : set (set β)} :
def
measurable
{α : Type u}
{β : Type v}
[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 β⦄, is_measurable t → is_measurable (f ⁻¹' t)
theorem
measurable_iff_le_map
{α : Type u}
{β : Type v}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
measurable f ↔ m₂ ≤ measurable_space.map f m₁
theorem
measurable_iff_comap_le
{α : Type u}
{β : Type v}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
measurable f ↔ measurable_space.comap f m₂ ≤ m₁
theorem
subsingleton.measurable
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
[subsingleton α]
{f : α → β} :
theorem
measurable.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{g : β → γ}
{f : α → β}
(hg : measurable g)
(hf : measurable f) :
measurable (g ∘ f)
theorem
measurable.mono
{α : Type u}
{β : Type v}
{ma ma' : measurable_space α}
{mb mb' : measurable_space β}
{f : α → β}
(hf : measurable f)
(ha : ma ≤ ma')
(hb : mb' ≤ mb) :
theorem
measurable_generate_from
{α : Type u}
{β : Type v}
[measurable_space α]
{s : set (set β)}
{f : α → β}
(h : ∀ (t : set β), t ∈ s → is_measurable (f ⁻¹' t)) :
theorem
measurable.piecewise
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{s : set α}
{_x : decidable_pred s}
{f g : α → β}
(hs : is_measurable s)
(hf : measurable f)
(hg : measurable g) :
measurable (s.piecewise f g)
@[simp]
theorem
measurable_const
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{a : α} :
measurable (λ (b : β), a)
theorem
measurable.indicator
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
[has_zero β]
{s : set α}
{f : α → β}
(hf : measurable f)
(hs : is_measurable s) :
measurable (s.indicator f)
theorem
measurable_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_zero α]
[measurable_space β] :
theorem
measurable_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[has_one α]
[measurable_space β] :
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem
measurable_to_encodable
{α : Type u}
{β : Type v}
[encodable α]
[measurable_space α]
[measurable_space β]
{f : β → α}
(h : ∀ (y : β), is_measurable (f ⁻¹' {f y})) :
theorem
measurable_to_nat
{α : Type u}
[measurable_space α]
{f : α → ℕ}
(a : ∀ (y : α), is_measurable (f ⁻¹' {f y})) :
theorem
measurable_find_greatest'
{α : Type u}
[measurable_space α]
{p : α → ℕ → Prop}
{N : ℕ}
(hN : ∀ (k : ℕ), k ≤ N → is_measurable {x : α | nat.find_greatest (p x) N = k}) :
measurable (λ (x : α), nat.find_greatest (p x) N)
theorem
measurable_find_greatest
{α : Type u}
[measurable_space α]
{p : α → ℕ → Prop}
{N : ℕ}
(hN : ∀ (k : ℕ), k ≤ N → is_measurable {x : α | p x k}) :
measurable (λ (x : α), nat.find_greatest (p x) N)
theorem
measurable_find
{α : Type u}
[measurable_space α]
{p : α → ℕ → Prop}
(hp : ∀ (x : α), ∃ (N : ℕ), p x N)
(hm : ∀ (k : ℕ), is_measurable {x : α | p x k}) :
measurable (λ (x : α), nat.find _)
@[instance]
Equations
theorem
measurable.subtype_coe
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{p : β → Prop}
{f : α → subtype p}
(hf : measurable f) :
measurable (λ (a : α), ↑(f a))
theorem
measurable.subtype_mk
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{p : β → Prop}
{f : α → β}
(hf : measurable f)
{h : ∀ (x : α), p (f x)} :
measurable (λ (x : α), ⟨f x, _⟩)
theorem
is_measurable.subtype_image
{α : Type u}
[measurable_space α]
{s : set α}
{t : set ↥s}
(hs : is_measurable s)
(a : is_measurable t) :
is_measurable (coe '' t)
theorem
measurable_of_measurable_union_cover
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{f : α → β}
(s t : set α)
(hs : is_measurable s)
(ht : is_measurable t)
(h : set.univ ⊆ s ∪ t)
(hc : measurable (λ (a : ↥s), f ↑a))
(hd : measurable (λ (a : ↥t), f ↑a)) :
theorem
measurable_of_measurable_on_compl_singleton
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
[measurable_singleton_class α]
{f : α → β}
(a : α)
(hf : measurable (set.restrict f {x : α | x ≠ a})) :
@[instance]
def
prod.measurable_space
{α : Type u}
{β : Type v}
[m₁ : measurable_space α]
[m₂ : measurable_space β] :
measurable_space (α × β)
Equations
theorem
measurable.fst
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β × γ}
(hf : measurable f) :
measurable (λ (a : α), (f a).fst)
theorem
measurable.snd
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β × γ}
(hf : measurable f) :
measurable (λ (a : α), (f a).snd)
theorem
measurable.prod
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β × γ}
(hf₁ : measurable (λ (a : α), (f a).fst))
(hf₂ : measurable (λ (a : α), (f a).snd)) :
theorem
measurable_prod
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β × γ} :
measurable f ↔ measurable (λ (a : α), (f a).fst) ∧ measurable (λ (a : α), (f a).snd)
theorem
measurable.prod_mk
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β}
{g : α → γ}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), (f a, g a))
theorem
measurable_prod_mk_left
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{x : α} :
measurable (prod.mk x)
theorem
measurable_prod_mk_right
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{y : β} :
measurable (λ (x : α), (x, y))
theorem
measurable.of_uncurry_left
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β → γ}
(hf : measurable (function.uncurry f))
{x : α} :
measurable (f x)
theorem
measurable.of_uncurry_right
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → β → γ}
(hf : measurable (function.uncurry f))
{y : β} :
measurable (λ (x : α), f x y)
theorem
measurable_swap_iff
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α × β → γ} :
measurable (f ∘ prod.swap) ↔ measurable f
theorem
is_measurable.prod
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{s : set α}
{t : set β}
(hs : is_measurable s)
(ht : is_measurable t) :
is_measurable (s.prod t)
theorem
is_measurable_prod_of_nonempty
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{s : set α}
{t : set β}
(h : (s.prod t).nonempty) :
is_measurable (s.prod t) ↔ is_measurable s ∧ is_measurable t
theorem
is_measurable_prod
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{s : set α}
{t : set β} :
is_measurable (s.prod t) ↔ is_measurable s ∧ is_measurable t ∨ s = ∅ ∨ t = ∅
theorem
is_measurable_swap_iff
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{s : set (α × β)} :
is_measurable (prod.swap ⁻¹' s) ↔ is_measurable s
@[instance]
def
measurable_space.pi
{α : Type u}
{β : α → Type v}
[m : Π (a : α), measurable_space (β a)] :
measurable_space (Π (a : α), β a)
Equations
- measurable_space.pi = ⨆ (a : α), measurable_space.comap (λ (b : Π (a : α), β a), b a) (m a)
theorem
measurable_pi_apply
{α : Type u}
{β : α → Type v}
[Π (a : α), measurable_space (β a)]
(a : α) :
measurable (λ (f : Π (a : α), β a), f a)
theorem
measurable_pi_lambda
{α : Type u}
{β : α → Type v}
{γ : Type w}
[Π (a : α), measurable_space (β a)]
[measurable_space γ]
(f : γ → Π (a : α), β a)
(hf : ∀ (a : α), measurable (λ (c : γ), f c a)) :
@[instance]
def
sum.measurable_space
{α : Type u}
{β : Type v}
[m₁ : measurable_space α]
[m₂ : measurable_space β] :
measurable_space (α ⊕ β)
Equations
theorem
measurable_sum
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α ⊕ β → γ}
(hl : measurable (f ∘ sum.inl))
(hr : measurable (f ∘ sum.inr)) :
theorem
measurable.sum_rec
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : α → γ}
{g : β → γ}
(hf : measurable f)
(hg : measurable g) :
measurable (sum.rec f g)
theorem
is_measurable.inl_image
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{s : set α}
(hs : is_measurable s) :
is_measurable (sum.inl '' s)
theorem
is_measurable_range_inl
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β] :
theorem
is_measurable_inr_image
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
{s : set β}
(hs : is_measurable s) :
is_measurable (sum.inr '' s)
theorem
is_measurable_range_inr
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β] :
@[instance]
Equations
- sigma.measurable_space = ⨅ (a : α), measurable_space.map (sigma.mk a) (m a)
structure
measurable_equiv
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[measurable_space β] :
Type (max u_1 u_2)
- to_equiv : α ≃ β
- measurable_to_fun : measurable c.to_equiv.to_fun
- measurable_inv_fun : measurable c.to_equiv.inv_fun
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
@[instance]
def
measurable_equiv.has_coe_to_fun
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[measurable_space β] :
Equations
- measurable_equiv.has_coe_to_fun α β = {F := λ (_x : measurable_equiv α β), α → β, coe := λ (e : measurable_equiv α β), ⇑(e.to_equiv)}
theorem
measurable_equiv.coe_eq
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : measurable_equiv α β) :
Any measurable space is equivalent to itself.
Equations
- measurable_equiv.refl α = {to_equiv := equiv.refl α, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.trans
{α : Type u}
{β : Type v}
{γ : Type w}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
(ab : measurable_equiv α β)
(bc : measurable_equiv β γ) :
measurable_equiv α γ
The composition of equivalences between measurable spaces.
Equations
- ab.trans bc = {to_equiv := ab.to_equiv.trans bc.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}
theorem
measurable_equiv.trans_to_equiv
{γ : Type w}
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
(e : measurable_equiv α β)
(f : measurable_equiv β γ) :
def
measurable_equiv.symm
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
(ab : measurable_equiv α β) :
measurable_equiv β α
The inverse of an equivalence between measurable spaces.
Equations
- ab.symm = {to_equiv := ab.to_equiv.symm, measurable_to_fun := _, measurable_inv_fun := _}
theorem
measurable_equiv.symm_to_equiv
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : measurable_equiv α β) :
def
measurable_equiv.cast
{α β : Type u_1}
[i₁ : measurable_space α]
[i₂ : measurable_space β]
(h : α = β)
(hi : i₁ == i₂) :
measurable_equiv α β
Equal measurable spaces are equivalent.
Equations
- measurable_equiv.cast h hi = {to_equiv := equiv.cast h, measurable_to_fun := _, measurable_inv_fun := _}
theorem
measurable_equiv.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : measurable_equiv α β) :
theorem
measurable_equiv.measurable_coe_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : β → γ}
(e : measurable_equiv α β) :
measurable (f ∘ ⇑e) ↔ measurable f
def
measurable_equiv.prod_congr
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
[measurable_space δ]
(ab : measurable_equiv α β)
(cd : measurable_equiv γ δ) :
measurable_equiv (α × γ) (β × δ)
Products of equivalent measurable spaces are equivalent.
Equations
- ab.prod_congr cd = {to_equiv := ab.to_equiv.prod_congr cd.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.prod_comm
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β] :
measurable_equiv (α × β) (β × α)
Products of measurable spaces are symmetric.
Equations
- measurable_equiv.prod_comm = {to_equiv := equiv.prod_comm α β, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.sum_congr
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
[measurable_space δ]
(ab : measurable_equiv α β)
(cd : measurable_equiv γ δ) :
measurable_equiv (α ⊕ γ) (β ⊕ δ)
Sums of measurable spaces are symmetric.
Equations
- ab.sum_congr cd = {to_equiv := ab.to_equiv.sum_congr cd.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.set.prod
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
(s : set α)
(t : set β) :
set.prod s t ≃ (s × t) as measurable spaces.
Equations
- measurable_equiv.set.prod s t = {to_equiv := equiv.set.prod s t, measurable_to_fun := _, measurable_inv_fun := _}
univ α ≃ α as measurable spaces.
Equations
- measurable_equiv.set.univ α = {to_equiv := equiv.set.univ α, measurable_to_fun := _, measurable_inv_fun := _}
{a} ≃ unit as measurable spaces.
Equations
- measurable_equiv.set.singleton a = {to_equiv := equiv.set.singleton a, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.set.image
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
(f : α → β)
(s : set α)
(hf : function.injective f)
(hfm : measurable f)
(hfi : ∀ (s : set α), is_measurable s → is_measurable (f '' s)) :
measurable_equiv ↥s ↥(f '' s)
A set is equivalent to its image under a function f as measurable spaces,
if f is an injective measurable function that sends measurable sets to measurable sets.
Equations
- measurable_equiv.set.image f s hf hfm hfi = {to_equiv := equiv.set.image f s hf, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.set.range
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β]
(f : α → β)
(hf : function.injective f)
(hfm : measurable f)
(hfi : ∀ (s : set α), is_measurable s → is_measurable (f '' s)) :
measurable_equiv α ↥(set.range f)
The domain of f is equivalent to its range as measurable spaces,
if f is an injective measurable function that sends measurable sets to measurable sets.
Equations
- measurable_equiv.set.range f hf hfm hfi = (measurable_equiv.set.univ α).symm.trans ((measurable_equiv.set.image f set.univ hf hfm hfi).trans (measurable_equiv.cast _ _))
def
measurable_equiv.set.range_inl
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β] :
α is equivalent to its image in α ⊕ β as measurable spaces.
Equations
- measurable_equiv.set.range_inl = {to_equiv := {to_fun := λ (ab : ↥(set.range sum.inl)), measurable_equiv.set.range_inl._match_1 ab, inv_fun := λ (a : α), ⟨sum.inl a, _⟩, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
- measurable_equiv.set.range_inl._match_1 ⟨sum.inr b, p⟩ = have this : false, from _, this.elim
- measurable_equiv.set.range_inl._match_1 ⟨sum.inl a, _x⟩ = a
def
measurable_equiv.set.range_inr
{α : Type u}
{β : Type v}
[measurable_space α]
[measurable_space β] :
β is equivalent to its image in α ⊕ β as measurable spaces.
Equations
- measurable_equiv.set.range_inr = {to_equiv := {to_fun := λ (ab : ↥(set.range sum.inr)), measurable_equiv.set.range_inr._match_1 ab, inv_fun := λ (b : β), ⟨sum.inr b, _⟩, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
- measurable_equiv.set.range_inr._match_1 ⟨sum.inr b, _x⟩ = b
- measurable_equiv.set.range_inr._match_1 ⟨sum.inl a, p⟩ = have this : false, from _, this.elim
def
measurable_equiv.sum_prod_distrib
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
[measurable_space α]
[measurable_space β]
[measurable_space γ] :
Products distribute over sums (on the right) as measurable spaces.
Equations
- measurable_equiv.sum_prod_distrib α β γ = {to_equiv := equiv.sum_prod_distrib α β γ, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.prod_sum_distrib
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
[measurable_space α]
[measurable_space β]
[measurable_space γ] :
Products distribute over sums (on the left) as measurable spaces.
def
measurable_equiv.sum_prod_sum
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
(δ : Type u_4)
[measurable_space α]
[measurable_space β]
[measurable_space γ]
[measurable_space δ] :
Products distribute over sums as measurable spaces.
Equations
- measurable_equiv.sum_prod_sum α β γ δ = (measurable_equiv.sum_prod_distrib α β (γ ⊕ δ)).trans ((measurable_equiv.prod_sum_distrib α γ δ).sum_congr (measurable_equiv.prod_sum_distrib β γ δ))
A pi-system is a collection of subsets of α that is closed under intersections of sets that
are not disjoint. Usually it is also required that the collection is nonempty, but we don't do
that here.
- has : set α → Prop
- has_empty : c.has ∅
- has_compl : ∀ {a : set α}, c.has a → c.has aᶜ
- has_Union_nat : ∀ {f : ℕ → set α}, pairwise (disjoint on f) → (∀ (i : ℕ), c.has (f i)) → c.has (⋃ (i : ℕ), f i)
A Dynkin system is a collection of subsets of a type α that contains the empty set,
is closed under complementation and under countable union of pairwise disjoint sets.
The disjointness condition is the only difference with σ-algebras.
The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated by intersection stable set systems.
A Dynkin system is also known as a "λ-system" or a "d-system".
@[ext]
theorem
measurable_space.dynkin_system.ext
{α : Type u}
{d₁ d₂ : measurable_space.dynkin_system α}
(a : ∀ (s : set α), d₁.has s ↔ d₂.has s) :
d₁ = d₂
theorem
measurable_space.dynkin_system.has_compl_iff
{α : Type u}
(d : measurable_space.dynkin_system α)
{a : set α} :
theorem
measurable_space.dynkin_system.has_univ
{α : Type u}
(d : measurable_space.dynkin_system α) :
theorem
measurable_space.dynkin_system.has_Union
{α : Type u}
(d : measurable_space.dynkin_system α)
{β : Type u_1}
[encodable β]
{f : β → set α}
(hd : pairwise (disjoint on f))
(h : ∀ (i : β), d.has (f i)) :
d.has (⋃ (i : β), f i)
theorem
measurable_space.dynkin_system.has_diff
{α : Type u}
(d : measurable_space.dynkin_system α)
{s₁ s₂ : set α}
(h₁ : d.has s₁)
(h₂ : d.has s₂)
(h : s₂ ⊆ s₁) :
@[instance]
Equations
- measurable_space.dynkin_system.partial_order = {le := λ (m₁ m₂ : measurable_space.dynkin_system α), m₁.has ≤ m₂.has, lt := preorder.lt._default (λ (m₁ m₂ : measurable_space.dynkin_system α), m₁.has ≤ m₂.has), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Every measurable space (σ-algebra) forms a Dynkin system
Equations
- measurable_space.dynkin_system.of_measurable_space m = {has := m.is_measurable', has_empty := _, has_compl := _, has_Union_nat := _}
theorem
measurable_space.dynkin_system.of_measurable_space_le_of_measurable_space_iff
{α : Type u}
{m₁ m₂ : measurable_space α} :
inductive
measurable_space.dynkin_system.generate_has
{α : Type u}
(s : set (set α))
(a : set α) :
Prop
- basic : ∀ {α : Type u} (s : set (set α)) (t : set α), t ∈ s → measurable_space.dynkin_system.generate_has s t
- empty : ∀ {α : Type u} (s : set (set α)), measurable_space.dynkin_system.generate_has s ∅
- compl : ∀ {α : Type u} (s : set (set α)) {a : set α}, measurable_space.dynkin_system.generate_has s a → measurable_space.dynkin_system.generate_has s aᶜ
- Union : ∀ {α : Type u} (s : set (set α)) {f : ℕ → set α}, pairwise (disjoint on f) → (∀ (i : ℕ), measurable_space.dynkin_system.generate_has s (f i)) → measurable_space.dynkin_system.generate_has s (⋃ (i : ℕ), f i)
The least Dynkin system containing a collection of basic sets. This inductive type gives the underlying collection of sets.
theorem
measurable_space.dynkin_system.generate_has_compl
{α : Type u}
{C : set (set α)}
{s : set α} :
The least Dynkin system containing a collection of basic sets.
Equations
- measurable_space.dynkin_system.generate s = {has := measurable_space.dynkin_system.generate_has s, has_empty := _, has_compl := _, has_Union_nat := _}
@[instance]
def
measurable_space.dynkin_system.to_measurable_space
{α : Type u}
(d : measurable_space.dynkin_system α)
(h_inter : ∀ (s₁ s₂ : set α), d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :
If a Dynkin system is closed under binary intersection, then it forms a σ-algebra.
Equations
- d.to_measurable_space h_inter = {is_measurable' := d.has, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}
theorem
measurable_space.dynkin_system.of_measurable_space_to_measurable_space
{α : Type u}
(d : measurable_space.dynkin_system α)
(h_inter : ∀ (s₁ s₂ : set α), d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :
def
measurable_space.dynkin_system.restrict_on
{α : Type u}
(d : measurable_space.dynkin_system α)
{s : set α}
(h : d.has s) :
If s is in a Dynkin system d, we can form the new Dynkin system {s ∩ t | t ∈ d}.
Equations
- d.restrict_on h = {has := λ (t : set α), d.has (t ∩ s), has_empty := _, has_compl := _, has_Union_nat := _}
theorem
measurable_space.dynkin_system.generate_le
{α : Type u}
(d : measurable_space.dynkin_system α)
{s : set (set α)}
(h : ∀ (t : set α), t ∈ s → d.has t) :
theorem
measurable_space.dynkin_system.generate_has_subset_generate_measurable
{α : Type u}
{C : set (set α)}
{s : set α}
(hs : (measurable_space.dynkin_system.generate C).has s) :
theorem
measurable_space.dynkin_system.generate_inter
{α : Type u}
{s : set (set α)}
(hs : is_pi_system s)
{t₁ t₂ : set α}
(ht₁ : (measurable_space.dynkin_system.generate s).has t₁)
(ht₂ : (measurable_space.dynkin_system.generate s).has t₂) :
(measurable_space.dynkin_system.generate s).has (t₁ ∩ t₂)
theorem
measurable_space.dynkin_system.generate_from_eq
{α : Type u}
{s : set (set α)}
(hs : is_pi_system s) :
If we have a collection of sets closed under binary intersections, then the Dynkin system it generates is equal to the σ-algebra it generates. This result is known as the π-λ theorem. A collection of sets closed under binary intersection is called a "π-system" if it is non-empty.
theorem
measurable_space.induction_on_inter
{α : Type u}
{C : set α → Prop}
{s : set (set α)}
[m : measurable_space α]
(h_eq : m = measurable_space.generate_from s)
(h_inter : is_pi_system s)
(h_empty : C ∅)
(h_basic : ∀ (t : set α), t ∈ s → C t)
(h_compl : ∀ (t : set α), is_measurable t → C t → C tᶜ)
(h_union : ∀ (f : ℕ → set α), pairwise (disjoint on f) → (∀ (i : ℕ), is_measurable (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i))
⦃t : set α⦄
(a : is_measurable t) :
C t
@[class]
- exists_measurable_subset : ∀ ⦃s : set α⦄, s ∈ f → (∃ (t : set α) (H : t ∈ f), is_measurable t ∧ t ⊆ s)
A filter f is measurably generates if each s ∈ f includes a measurable t ∈ f.
Instances
- filter.is_measurably_generated_bot
- filter.is_measurably_generated_top
- filter.inf_is_measurably_generated
- filter.infi_is_measurably_generated
- measure_theory.ae_is_measurably_generated
- nhds_is_measurably_generated
- nhds_within_Ici_is_measurably_generated
- nhds_within_Iic_is_measurably_generated
- at_top_is_measurably_generated
- at_bot_is_measurably_generated
- nhds_within_Ioi_is_measurably_generated
- nhds_within_Iio_is_measurably_generated
@[instance]
@[instance]
theorem
filter.eventually.exists_measurable_mem
{α : Type u}
[measurable_space α]
{f : filter α}
[f.is_measurably_generated]
{p : α → Prop}
(h : ∀ᶠ (x : α) in f, p x) :
∃ (s : set α) (H : s ∈ f), is_measurable s ∧ ∀ (x : α), x ∈ s → p x
@[instance]
def
filter.inf_is_measurably_generated
{α : Type u}
[measurable_space α]
(f g : filter α)
[f.is_measurably_generated]
[g.is_measurably_generated] :
(f ⊓ g).is_measurably_generated
theorem
filter.principal_is_measurably_generated_iff
{α : Type u}
[measurable_space α]
{s : set α} :
@[instance]
def
filter.infi_is_measurably_generated
{α : Type u}
{ι : Sort x}
[measurable_space α]
{f : ι → filter α}
[∀ (i : ι), (f i).is_measurably_generated] :
(⨅ (i : ι), f i).is_measurably_generated