Measurable spaces and measurable functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides properties of measurable spaces and the functions and isomorphisms
between them. The definition of a measurable space is in measure_theory.measurable_space_def.
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.
Notation #
- We write
α ≃ᵐ βfor measurable equivalences between the measurable spacesαandβ. This should not be confused with≃ₘwhich is used for diffeomorphisms between manifolds.
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, σ-algebra, measurable function, measurable equivalence, dynkin system, π-λ theorem, π-system
@[protected]
The forward image of a measurable space under a function. map f m contains the sets
s : set β whose preimage under f is measurable.
Equations
- measurable_space.map f m = {measurable_set' := λ (s : set β), measurable_set (f ⁻¹' s), measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}
@[simp]
theorem
measurable_space.map_id
{α : Type u_1}
{m : measurable_space α} :
measurable_space.map id m = m
@[simp]
theorem
measurable_space.map_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{f : α → β}
{g : β → γ} :
measurable_space.map g (measurable_space.map f m) = measurable_space.map (g ∘ f) m
@[protected]
The reverse image of a measurable 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 = {measurable_set' := λ (s : set α), ∃ (s' : set β), measurable_set s' ∧ f ⁻¹' s' = s, measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}
theorem
measurable_space.comap_eq_generate_from
{α : Type u_1}
{β : Type u_2}
(m : measurable_space β)
(f : α → β) :
measurable_space.comap f m = measurable_space.generate_from {t : set α | ∃ (s : set β), measurable_set s ∧ f ⁻¹' s = t}
@[simp]
@[simp]
theorem
measurable_space.comap_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{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_1}
{β : Type u_2}
{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_1}
{β : Type u_2}
{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_1}
{β : Type u_2}
{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_1}
{β : Type u_2}
{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_1}
{β : Type u_2}
{ι : Sort u_6}
{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_1}
{β : Type u_2}
{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_1}
{β : Type u_2}
{ι : Sort u_6}
{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_1}
{β : Type u_2}
{m : measurable_space α}
{f : α → β} :
measurable_space.comap f (measurable_space.map f m) ≤ m
theorem
measurable_space.le_map_comap
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{g : β → α} :
m ≤ measurable_space.map g (measurable_space.comap g m)
@[simp]
theorem
measurable_space.map_const
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
(b : β) :
measurable_space.map (λ (a : α), b) m = ⊤
@[simp]
theorem
measurable_space.comap_const
{α : Type u_1}
{β : Type u_2}
{m : measurable_space β}
(b : β) :
measurable_space.comap (λ (a : α), b) m = ⊥
theorem
measurable_iff_le_map
{α : Type u_1}
{β : Type u_2}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
measurable f ↔ m₂ ≤ measurable_space.map f m₁
theorem
measurable.le_map
{α : Type u_1}
{β : Type u_2}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
measurable f → m₂ ≤ measurable_space.map f m₁
Alias of the forward direction of measurable_iff_le_map.
theorem
measurable.of_le_map
{α : Type u_1}
{β : Type u_2}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
m₂ ≤ measurable_space.map f m₁ → measurable f
Alias of the reverse direction of measurable_iff_le_map.
theorem
measurable_iff_comap_le
{α : Type u_1}
{β : Type u_2}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
measurable f ↔ measurable_space.comap f m₂ ≤ m₁
theorem
measurable.comap_le
{α : Type u_1}
{β : Type u_2}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
measurable f → measurable_space.comap f m₂ ≤ m₁
Alias of the forward direction of measurable_iff_comap_le.
theorem
measurable.of_comap_le
{α : Type u_1}
{β : Type u_2}
{m₁ : measurable_space α}
{m₂ : measurable_space β}
{f : α → β} :
measurable_space.comap f m₂ ≤ m₁ → measurable f
Alias of the reverse direction of measurable_iff_comap_le.
theorem
measurable.mono
{α : Type u_1}
{β : Type u_2}
{ma ma' : measurable_space α}
{mb mb' : measurable_space β}
{f : α → β}
(hf : measurable f)
(ha : ma ≤ ma')
(hb : mb' ≤ mb) :
@[measurability]
theorem
measurable_generate_from
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{s : set (set β)}
{f : α → β}
(h : ∀ (t : set β), t ∈ s → measurable_set (f ⁻¹' t)) :
@[measurability]
theorem
subsingleton.measurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[measurable_space α]
[measurable_space β]
[subsingleton α] :
@[measurability]
theorem
measurable_of_subsingleton_codomain
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[subsingleton β]
(f : α → β) :
@[measurability]
theorem
measurable_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[has_zero α] :
@[measurability]
theorem
measurable_one
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[has_one α] :
theorem
measurable_of_empty
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[is_empty α]
(f : α → β) :
theorem
measurable_of_empty_codomain
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[is_empty β]
(f : α → β) :
theorem
measurable_const'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : β → α}
(hf : ∀ (x y : β), f x = f y) :
A version of measurable_const that assumes f x = f y for all x, y. This version works
for functions between empty types.
@[measurability]
theorem
measurable_nat_cast
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[has_nat_cast α]
(n : ℕ) :
@[measurability]
theorem
measurable_int_cast
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[has_int_cast α]
(n : ℤ) :
theorem
measurable_of_finite
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[finite α]
[measurable_singleton_class α]
(f : α → β) :
theorem
measurable_of_countable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[countable α]
[measurable_singleton_class α]
(f : α → β) :
@[measurability]
theorem
measurable.iterate
{α : Type u_1}
{m : measurable_space α}
{f : α → α}
(hf : measurable f)
(n : ℕ) :
@[measurability]
theorem
measurable_set_preimage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : measurable_space α}
{mβ : measurable_space β}
{t : set β}
(hf : measurable f)
(ht : measurable_set t) :
measurable_set (f ⁻¹' t)
@[measurability]
theorem
measurable.piecewise
{α : Type u_1}
{β : Type u_2}
{s : set α}
{f g : α → β}
{m : measurable_space α}
{mβ : measurable_space β}
{_x : decidable_pred (λ (_x : α), _x ∈ s)}
(hs : measurable_set s)
(hf : measurable f)
(hg : measurable g) :
measurable (s.piecewise f g)
theorem
measurable.ite
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{m : measurable_space α}
{mβ : measurable_space β}
{p : α → Prop}
{_x : decidable_pred p}
(hp : measurable_set {a : α | p a})
(hf : measurable f)
(hg : measurable g) :
measurable (λ (x : α), ite (p x) (f x) (g x))
this is slightly different from measurable.piecewise. It can be used to show
measurable (ite (x=0) 0 1) by
exact measurable.ite (measurable_set_singleton 0) measurable_const measurable_const,
but replacing measurable.ite by measurable.piecewise in that example proof does not work.
@[measurability]
theorem
measurable.indicator
{α : Type u_1}
{β : Type u_2}
{s : set α}
{f : α → β}
{m : measurable_space α}
{mβ : measurable_space β}
[has_zero β]
(hf : measurable f)
(hs : measurable_set s) :
measurable (s.indicator f)
@[measurability]
theorem
measurable_set_support
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : measurable_space α}
{mβ : measurable_space β}
[has_zero β]
[measurable_singleton_class β]
(hf : measurable f) :
@[measurability]
theorem
measurable_set_mul_support
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : measurable_space α}
{mβ : measurable_space β}
[has_one β]
[measurable_singleton_class β]
(hf : measurable f) :
theorem
measurable.measurable_of_countable_ne
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{m : measurable_space α}
{mβ : measurable_space β}
[measurable_singleton_class α]
(hf : measurable f)
(h : {x : α | f x ≠ g x}.countable) :
If a function coincides with a measurable function outside of a countable set, it is measurable.
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
theorem
measurable_to_countable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[countable α]
[measurable_space β]
{f : β → α}
(h : ∀ (y : β), measurable_set (f ⁻¹' {f y})) :
theorem
measurable_to_countable'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[countable α]
[measurable_space β]
{f : β → α}
(h : ∀ (x : α), measurable_set (f ⁻¹' {x})) :
@[measurability]
@[measurability]
theorem
measurable_to_nat
{α : Type u_1}
[measurable_space α]
{f : α → ℕ} :
(∀ (y : α), measurable_set (f ⁻¹' {f y})) → measurable f
theorem
measurable_to_bool
{α : Type u_1}
[measurable_space α]
{f : α → bool}
(h : measurable_set (f ⁻¹' {bool.tt})) :
theorem
measurable_to_prop
{α : Type u_1}
[measurable_space α]
{f : α → Prop}
(h : measurable_set (f ⁻¹' {true})) :
theorem
measurable_find_greatest'
{α : Type u_1}
[measurable_space α]
{p : α → ℕ → Prop}
[Π (x : α), decidable_pred (p x)]
{N : ℕ}
(hN : ∀ (k : ℕ), k ≤ N → measurable_set {x : α | nat.find_greatest (p x) N = k}) :
measurable (λ (x : α), nat.find_greatest (p x) N)
theorem
measurable_find_greatest
{α : Type u_1}
[measurable_space α]
{p : α → ℕ → Prop}
[Π (x : α), decidable_pred (p x)]
{N : ℕ}
(hN : ∀ (k : ℕ), k ≤ N → measurable_set {x : α | p x k}) :
measurable (λ (x : α), nat.find_greatest (p x) N)
theorem
measurable_find
{α : Type u_1}
[measurable_space α]
{p : α → ℕ → Prop}
[Π (x : α), decidable_pred (p x)]
(hp : ∀ (x : α), ∃ (N : ℕ), p x N)
(hm : ∀ (k : ℕ), measurable_set {x : α | p x k}) :
measurable (λ (x : α), nat.find _)
@[protected, instance]
def
quot.measurable_space
{α : Type u_1}
{r : α → α → Prop}
[m : measurable_space α] :
measurable_space (quot r)
Equations
- quot.measurable_space = measurable_space.map (quot.mk r) m
@[protected, instance]
Equations
@[protected, instance]
def
quotient_add_group.measurable_space
{G : Type u_1}
[add_group G]
[measurable_space G]
(S : add_subgroup G) :
measurable_space (G ⧸ S)
@[protected, instance]
def
quotient_group.measurable_space
{G : Type u_1}
[group G]
[measurable_space G]
(S : subgroup G) :
measurable_space (G ⧸ S)
theorem
measurable_set_quotient
{α : Type u_1}
[measurable_space α]
{s : setoid α}
{t : set (quotient s)} :
theorem
measurable_from_quotient
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{s : setoid α}
{f : quotient s → β} :
measurable f ↔ measurable (f ∘ quotient.mk')
@[measurability]
@[measurability]
@[measurability]
theorem
measurable_quot_mk
{α : Type u_1}
[measurable_space α]
{r : α → α → Prop} :
measurable (quot.mk r)
@[measurability]
theorem
quotient_add_group.measurable_coe
{G : Type u_1}
[add_group G]
[measurable_space G]
{S : add_subgroup G} :
@[measurability]
theorem
quotient_group.measurable_coe
{G : Type u_1}
[group G]
[measurable_space G]
{S : subgroup G} :
theorem
quotient_add_group.measurable_from_quotient
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[add_group G]
[measurable_space G]
{S : add_subgroup G}
{f : G ⧸ S → α} :
measurable f ↔ measurable (f ∘ coe)
theorem
quotient_group.measurable_from_quotient
{α : Type u_1}
[measurable_space α]
{G : Type u_2}
[group G]
[measurable_space G]
{S : subgroup G}
{f : G ⧸ S → α} :
measurable f ↔ measurable (f ∘ coe)
@[protected, instance]
Equations
@[measurability]
@[protected, instance]
def
subtype.measurable_singleton_class
{α : Type u_1}
[measurable_space α]
{p : α → Prop}
[measurable_singleton_class α] :
theorem
measurable_set.subtype_image
{α : Type u_1}
{m : measurable_space α}
{s : set α}
{t : set ↥s}
(hs : measurable_set s) :
measurable_set t → measurable_set (coe '' t)
@[measurability]
theorem
measurable.subtype_coe
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{p : β → Prop}
{f : α → subtype p}
(hf : measurable f) :
measurable (λ (a : α), ↑(f a))
@[measurability]
theorem
measurable.subtype_mk
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{p : β → Prop}
{f : α → β}
(hf : measurable f)
{h : ∀ (x : α), p (f x)} :
measurable (λ (x : α), ⟨f x, _⟩)
theorem
measurable_of_measurable_union_cover
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{f : α → β}
(s t : set α)
(hs : measurable_set s)
(ht : measurable_set t)
(h : set.univ ⊆ s ∪ t)
(hc : measurable (λ (a : ↥s), f ↑a))
(hd : measurable (λ (a : ↥t), f ↑a)) :
theorem
measurable_of_restrict_of_restrict_compl
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{f : α → β}
{s : set α}
(hs : measurable_set s)
(h₁ : measurable (s.restrict f))
(h₂ : measurable (sᶜ.restrict f)) :
theorem
measurable.dite
{α : Type u_1}
{β : Type u_2}
{s : set α}
{m : measurable_space α}
{mβ : measurable_space β}
[Π (x : α), decidable (x ∈ s)]
{f : ↥s → β}
(hf : measurable f)
{g : ↥sᶜ → β}
(hg : measurable g)
(hs : measurable_set s) :
theorem
measurable_of_measurable_on_compl_finite
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
[measurable_singleton_class α]
{f : α → β}
(s : set α)
(hs : s.finite)
(hf : measurable (sᶜ.restrict f)) :
theorem
measurable_of_measurable_on_compl_singleton
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
[measurable_singleton_class α]
{f : α → β}
(a : α)
(hf : measurable ({x : α | x ≠ a}.restrict f)) :
def
measurable_space.prod
{α : Type u_1}
{β : Type u_2}
(m₁ : measurable_space α)
(m₂ : measurable_space β) :
measurable_space (α × β)
A measurable_space structure on the product of two measurable spaces.
Equations
- m₁.prod m₂ = measurable_space.comap prod.fst m₁ ⊔ measurable_space.comap prod.snd m₂
@[protected, instance]
def
prod.measurable_space
{α : Type u_1}
{β : Type u_2}
[m₁ : measurable_space α]
[m₂ : measurable_space β] :
measurable_space (α × β)
Equations
- prod.measurable_space = m₁.prod m₂
@[measurability]
theorem
measurable_fst
{α : Type u_1}
{β : Type u_2}
{ma : measurable_space α}
{mb : measurable_space β} :
@[measurability]
theorem
measurable_snd
{α : Type u_1}
{β : Type u_2}
{ma : measurable_space α}
{mb : measurable_space β} :
theorem
measurable.fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → β × γ}
(hf : measurable f) :
measurable (λ (a : α), (f a).fst)
theorem
measurable.snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → β × γ}
(hf : measurable f) :
measurable (λ (a : α), (f a).snd)
@[measurability]
theorem
measurable.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → β × γ}
(hf₁ : measurable (λ (a : α), (f a).fst))
(hf₂ : measurable (λ (a : α), (f a).snd)) :
theorem
measurable.prod_mk
{α : Type u_1}
{m : measurable_space α}
{β : Type u_2}
{γ : Type u_3}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → β}
{g : α → γ}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (a : α), (f a, g a))
theorem
measurable.prod_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
[measurable_space δ]
{f : α → β}
{g : γ → δ}
(hf : measurable f)
(hg : measurable g) :
measurable (prod.map f g)
theorem
measurable_prod_mk_left
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{x : α} :
measurable (prod.mk x)
theorem
measurable_prod_mk_right
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{y : β} :
measurable (λ (x : α), (x, y))
theorem
measurable.of_uncurry_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → β → γ}
(hf : measurable (function.uncurry f))
{x : α} :
measurable (f x)
theorem
measurable.of_uncurry_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → β → γ}
(hf : measurable (function.uncurry f))
{y : β} :
measurable (λ (x : α), f x y)
theorem
measurable_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → β × γ} :
measurable f ↔ measurable (λ (a : α), (f a).fst) ∧ measurable (λ (a : α), (f a).snd)
@[measurability]
theorem
measurable_swap
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β} :
theorem
measurable_swap_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α × β → γ} :
measurable (f ∘ prod.swap) ↔ measurable f
@[measurability]
theorem
measurable_set.prod
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{s : set α}
{t : set β}
(hs : measurable_set s)
(ht : measurable_set t) :
measurable_set (s ×ˢ t)
theorem
measurable_set_prod_of_nonempty
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{s : set α}
{t : set β}
(h : (s ×ˢ t).nonempty) :
measurable_set (s ×ˢ t) ↔ measurable_set s ∧ measurable_set t
theorem
measurable_set_prod
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{s : set α}
{t : set β} :
measurable_set (s ×ˢ t) ↔ measurable_set s ∧ measurable_set t ∨ s = ∅ ∨ t = ∅
theorem
measurable_set_swap_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{s : set (α × β)} :
@[protected, instance]
def
prod.measurable_singleton_class
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
[measurable_singleton_class α]
[measurable_singleton_class β] :
measurable_singleton_class (α × β)
theorem
measurable_from_prod_countable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
[countable β]
[measurable_singleton_class β]
{mγ : measurable_space γ}
{f : α × β → γ}
(hf : ∀ (y : β), measurable (λ (x : α), f (x, y))) :
@[measurability]
theorem
measurable.find
{α : Type u_1}
{β : Type u_2}
{mβ : measurable_space β}
{m : measurable_space α}
{f : ℕ → α → β}
{p : ℕ → α → Prop}
[Π (n : ℕ), decidable_pred (p n)]
(hf : ∀ (n : ℕ), measurable (f n))
(hp : ∀ (n : ℕ), measurable_set {x : α | p n x})
(h : ∀ (x : α), ∃ (n : ℕ), p n x) :
measurable (λ (x : α), f (nat.find _) x)
A piecewise function on countably many pieces is measurable if all the data is measurable.
theorem
exists_measurable_piecewise_nat
{α : Type u_1}
{β : Type u_2}
{mβ : measurable_space β}
{m : measurable_space α}
(t : ℕ → set β)
(t_meas : ∀ (n : ℕ), measurable_set (t n))
(t_disj : pairwise (disjoint on t))
(g : ℕ → β → α)
(hg : ∀ (n : ℕ), measurable (g n)) :
Given countably many disjoint measurable sets t n and countably many measurable
functions g n, one can construct a measurable function that coincides with g n on t n.
@[protected, instance]
def
measurable_space.pi
{δ : Type u_4}
{π : δ → Type u_7}
[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_iff
{α : Type u_1}
{δ : Type u_4}
{π : δ → Type u_7}
[measurable_space α]
[Π (a : δ), measurable_space (π a)]
{g : α → Π (a : δ), π a} :
measurable g ↔ ∀ (a : δ), measurable (λ (x : α), g x a)
@[measurability]
theorem
measurable_pi_apply
{δ : Type u_4}
{π : δ → Type u_7}
[Π (a : δ), measurable_space (π a)]
(a : δ) :
measurable (λ (f : Π (a : δ), π a), f a)
@[measurability]
theorem
measurable.eval
{α : Type u_1}
{δ : Type u_4}
{π : δ → Type u_7}
[measurable_space α]
[Π (a : δ), measurable_space (π a)]
{a : δ}
{g : α → Π (a : δ), π a}
(hg : measurable g) :
measurable (λ (x : α), g x a)
@[measurability]
theorem
measurable_pi_lambda
{α : Type u_1}
{δ : Type u_4}
{π : δ → Type u_7}
[measurable_space α]
[Π (a : δ), measurable_space (π a)]
(f : α → Π (a : δ), π a)
(hf : ∀ (a : δ), measurable (λ (c : α), f c a)) :
@[measurability]
theorem
measurable_update
{δ : Type u_4}
{π : δ → Type u_7}
[Π (a : δ), measurable_space (π a)]
(f : Π (a : δ), π a)
{a : δ}
[decidable_eq δ] :
measurable (function.update f a)
The function update f a : π a → Π a, π a is always measurable.
This doesn't require f to be measurable.
This should not be confused with the statement that update f a x is measurable.
@[measurability]
theorem
measurable_set.pi
{δ : Type u_4}
{π : δ → Type u_7}
[Π (a : δ), measurable_space (π a)]
{s : set δ}
{t : Π (i : δ), set (π i)}
(hs : s.countable)
(ht : ∀ (i : δ), i ∈ s → measurable_set (t i)) :
measurable_set (s.pi t)
theorem
measurable_set.univ_pi
{δ : Type u_4}
{π : δ → Type u_7}
[Π (a : δ), measurable_space (π a)]
[countable δ]
{t : Π (i : δ), set (π i)}
(ht : ∀ (i : δ), measurable_set (t i)) :
measurable_set (set.univ.pi t)
theorem
measurable_set_pi_of_nonempty
{δ : Type u_4}
{π : δ → Type u_7}
[Π (a : δ), measurable_space (π a)]
{s : set δ}
{t : Π (i : δ), set (π i)}
(hs : s.countable)
(h : (s.pi t).nonempty) :
measurable_set (s.pi t) ↔ ∀ (i : δ), i ∈ s → measurable_set (t i)
@[protected, instance]
def
pi.measurable_singleton_class
{δ : Type u_4}
{π : δ → Type u_7}
[Π (a : δ), measurable_space (π a)]
[countable δ]
[∀ (a : δ), measurable_singleton_class (π a)] :
measurable_singleton_class (Π (a : δ), π a)
@[measurability]
theorem
measurable_pi_equiv_pi_subtype_prod_symm
{δ : Type u_4}
(π : δ → Type u_7)
[Π (a : δ), measurable_space (π a)]
(p : δ → Prop)
[decidable_pred p] :
@[measurability]
theorem
measurable_pi_equiv_pi_subtype_prod
{δ : Type u_4}
(π : δ → Type u_7)
[Π (a : δ), measurable_space (π a)]
(p : δ → Prop)
[decidable_pred p] :
@[protected, instance]
def
tprod.measurable_space
{δ : Type u_4}
(π : δ → Type u_1)
[Π (x : δ), measurable_space (π x)]
(l : list δ) :
measurable_space (list.tprod π l)
Equations
theorem
measurable_tprod_mk
{δ : Type u_4}
{π : δ → Type u_7}
[Π (x : δ), measurable_space (π x)]
(l : list δ) :
theorem
measurable_tprod_elim
{δ : Type u_4}
{π : δ → Type u_7}
[Π (x : δ), measurable_space (π x)]
[decidable_eq δ]
{l : list δ}
{i : δ}
(hi : i ∈ l) :
measurable (λ (v : list.tprod π l), v.elim hi)
theorem
measurable_tprod_elim'
{δ : Type u_4}
{π : δ → Type u_7}
[Π (x : δ), measurable_space (π x)]
[decidable_eq δ]
{l : list δ}
(h : ∀ (i : δ), i ∈ l) :
theorem
measurable_set.tprod
{δ : Type u_4}
{π : δ → Type u_7}
[Π (x : δ), measurable_space (π x)]
(l : list δ)
{s : Π (i : δ), set (π i)}
(hs : ∀ (i : δ), measurable_set (s i)) :
measurable_set (set.tprod l s)
@[protected, instance]
def
sum.measurable_space
{α : Type u_1}
{β : Type u_2}
[m₁ : measurable_space α]
[m₂ : measurable_space β] :
measurable_space (α ⊕ β)
Equations
@[measurability]
@[measurability]
theorem
measurable_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α ⊕ β → γ}
(hl : measurable (f ∘ sum.inl))
(hr : measurable (f ∘ sum.inr)) :
@[measurability]
theorem
measurable.sum_elim
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
{f : α → γ}
{g : β → γ}
(hf : measurable f)
(hg : measurable g) :
measurable (sum.elim f g)
theorem
measurable_set.inl_image
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{s : set α}
(hs : measurable_set s) :
measurable_set (sum.inl '' s)
theorem
measurable_set_inr_image
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{mβ : measurable_space β}
{s : set β}
(hs : measurable_set s) :
measurable_set (sum.inr '' s)
theorem
measurable_set_range_inl
{α : Type u_1}
{β : Type u_2}
{mβ : measurable_space β}
[measurable_space α] :
theorem
measurable_set_range_inr
{α : Type u_1}
{β : Type u_2}
{mβ : measurable_space β}
[measurable_space α] :
@[protected, instance]
def
sigma.measurable_space
{α : Type u_1}
{β : α → Type u_2}
[m : Π (a : α), measurable_space (β a)] :
Equations
- sigma.measurable_space = ⨅ (a : α), measurable_space.map (sigma.mk a) (m a)
@[simp]
theorem
measurable_set_set_of
{α : Type u_1}
{p : α → Prop}
[measurable_space α] :
measurable_set {a : α | p a} ↔ measurable p
@[simp]
theorem
measurable_mem
{α : Type u_1}
{s : set α}
[measurable_space α] :
measurable (λ (_x : α), _x ∈ s) ↔ measurable_set s
theorem
measurable.set_of
{α : Type u_1}
{p : α → Prop}
[measurable_space α] :
measurable p → measurable_set {a : α | p a}
Alias of the reverse direction of measurable_set_set_of.
theorem
measurable_set.mem
{α : Type u_1}
{s : set α}
[measurable_space α] :
measurable_set s → measurable (λ (_x : α), _x ∈ s)
Alias of the reverse direction of measurable_mem.
@[simp]
theorem
measurable_space.generate_from_singleton
{α : Type u_1}
(s : set α) :
measurable_space.generate_from {s} = measurable_space.comap (λ (_x : α), _x ∈ s) ⊤
The sigma-algebra generated by a single set s is {∅, s, sᶜ, univ}.
structure
measurable_embedding
{α : Type u_7}
{β : Type u_8}
[measurable_space α]
[measurable_space β]
(f : α → β) :
Prop
- injective : function.injective f
- measurable : measurable f
- measurable_set_image' : ∀ ⦃s : set α⦄, measurable_set s → measurable_set (f '' s)
A map f : α → β is called a measurable embedding if it is injective, measurable, and sends
measurable sets to measurable sets. The latter assumption can be replaced with “f has measurable
inverse g : range f → α”, see measurable_embedding.measurable_range_splitting,
measurable_embedding.of_measurable_inverse_range, and
measurable_embedding.of_measurable_inverse.
One more interpretation: f is a measurable embedding if it defines a measurable equivalence to its
range and the range is a measurable set. One implication is formalized as
measurable_embedding.equiv_range; the other one follows from
measurable_equiv.measurable_embedding, measurable_embedding.subtype_coe, and
measurable_embedding.comp.
theorem
measurable_embedding.measurable_set_image
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
[measurable_space β]
{f : α → β}
(hf : measurable_embedding f)
{s : set α} :
measurable_set (f '' s) ↔ measurable_set s
theorem
measurable_embedding.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : measurable_space α}
[measurable_space β]
[measurable_space γ]
{f : α → β}
{g : β → γ}
(hg : measurable_embedding g)
(hf : measurable_embedding f) :
measurable_embedding (g ∘ f)
theorem
measurable_embedding.subtype_coe
{α : Type u_1}
{mα : measurable_space α}
{s : set α}
(hs : measurable_set s) :
theorem
measurable_embedding.measurable_set_range
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
[measurable_space β]
{f : α → β}
(hf : measurable_embedding f) :
theorem
measurable_embedding.measurable_set_preimage
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
[measurable_space β]
{f : α → β}
(hf : measurable_embedding f)
{s : set β} :
measurable_set (f ⁻¹' s) ↔ measurable_set (s ∩ set.range f)
theorem
measurable_embedding.measurable_range_splitting
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
[measurable_space β]
{f : α → β}
(hf : measurable_embedding f) :
theorem
measurable_embedding.measurable_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : measurable_space α}
[measurable_space β]
[measurable_space γ]
{f : α → β}
(hf : measurable_embedding f)
{g : α → γ}
{g' : β → γ}
(hg : measurable g)
(hg' : measurable g') :
measurable (function.extend f g g')
theorem
measurable_embedding.exists_measurable_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : measurable_space α}
[measurable_space β]
[measurable_space γ]
{f : α → β}
(hf : measurable_embedding f)
{g : α → γ}
(hg : measurable g)
(hne : β → nonempty γ) :
theorem
measurable_embedding.measurable_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : measurable_space α}
[measurable_space β]
[measurable_space γ]
{f : α → β}
{g : β → γ}
(hg : measurable_embedding g) :
measurable (g ∘ f) ↔ measurable f
theorem
measurable_set.exists_measurable_proj
{α : Type u_1}
{m : measurable_space α}
{s : set α}
(hs : measurable_set s)
(hne : s.nonempty) :
structure
measurable_equiv
(α : Type u_7)
(β : Type u_8)
[measurable_space α]
[measurable_space β] :
Type (max u_7 u_8)
- to_equiv : α ≃ β
- measurable_to_fun : measurable ⇑(self.to_equiv)
- measurable_inv_fun : measurable ⇑(self.to_equiv.symm)
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
Instances for measurable_equiv
- measurable_equiv.has_sizeof_inst
- measurable_equiv.has_coe_to_fun
- measurable_equiv.inhabited
@[protected, instance]
def
measurable_equiv.has_coe_to_fun
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[measurable_space β] :
has_coe_to_fun (α ≃ᵐ β) (λ (_x : α ≃ᵐ β), α → β)
@[simp]
theorem
measurable_equiv.coe_to_equiv
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
@[protected, measurability]
theorem
measurable_equiv.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
@[simp]
theorem
measurable_equiv.coe_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ β)
(h1 : measurable ⇑e)
(h2 : measurable ⇑(e.symm)) :
⇑{to_equiv := e, measurable_to_fun := h1, measurable_inv_fun := h2} = ⇑e
Any measurable space is equivalent to itself.
Equations
- measurable_equiv.refl α = {to_equiv := equiv.refl α, measurable_to_fun := _, measurable_inv_fun := _}
@[protected, instance]
Equations
- measurable_equiv.inhabited = {default := measurable_equiv.refl α _inst_1}
def
measurable_equiv.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ) :
α ≃ᵐ γ
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 := _}
def
measurable_equiv.symm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(ab : α ≃ᵐ β) :
β ≃ᵐ α
The inverse of an equivalence between measurable spaces.
Equations
- ab.symm = {to_equiv := ab.to_equiv.symm, measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
theorem
measurable_equiv.coe_to_equiv_symm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
def
measurable_equiv.simps.apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(h : α ≃ᵐ β) :
α → β
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
measurable_equiv.simps.symm_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(h : α ≃ᵐ β) :
β → α
See Note [custom simps projection]
Equations
theorem
measurable_equiv.to_equiv_injective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β] :
@[ext]
theorem
measurable_equiv.ext
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{e₁ e₂ : α ≃ᵐ β}
(h : ⇑e₁ = ⇑e₂) :
e₁ = e₂
@[simp]
theorem
measurable_equiv.symm_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ β)
(h1 : measurable ⇑e)
(h2 : measurable ⇑(e.symm)) :
{to_equiv := e, measurable_to_fun := h1, measurable_inv_fun := h2}.symm = {to_equiv := e.symm, measurable_to_fun := h2, measurable_inv_fun := h1}
@[simp]
@[simp]
theorem
measurable_equiv.trans_to_equiv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ) :
@[simp]
theorem
measurable_equiv.trans_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
(ᾰ : α) :
@[simp]
theorem
measurable_equiv.refl_apply
(α : Type u_1)
[measurable_space α]
(a : α) :
⇑(measurable_equiv.refl α) a = a
@[simp]
@[simp]
theorem
measurable_equiv.symm_comp_self
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
@[simp]
theorem
measurable_equiv.self_comp_symm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
@[simp]
theorem
measurable_equiv.apply_symm_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β)
(y : β) :
@[simp]
theorem
measurable_equiv.symm_apply_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β)
(x : α) :
@[simp]
theorem
measurable_equiv.symm_trans_self
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
e.symm.trans e = measurable_equiv.refl β
@[simp]
theorem
measurable_equiv.self_trans_symm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
e.trans e.symm = measurable_equiv.refl α
@[protected]
theorem
measurable_equiv.surjective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
@[protected]
theorem
measurable_equiv.bijective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
@[protected]
theorem
measurable_equiv.injective
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
@[simp]
theorem
measurable_equiv.symm_preimage_preimage
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β)
(s : set β) :
theorem
measurable_equiv.image_eq_preimage
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β)
(s : set α) :
@[simp]
theorem
measurable_equiv.measurable_set_preimage
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β)
{s : set β} :
measurable_set (⇑e ⁻¹' s) ↔ measurable_set s
@[simp]
theorem
measurable_equiv.measurable_set_image
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β)
{s : set α} :
measurable_set (⇑e '' s) ↔ measurable_set s
@[simp]
theorem
measurable_equiv.map_eq
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
measurable_space.map ⇑e _inst_1 = _inst_2
@[protected]
theorem
measurable_equiv.measurable_embedding
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β) :
A measurable equivalence is a measurable embedding.
@[protected]
def
measurable_equiv.cast
{α β : Type u_1}
[i₁ : measurable_space α]
[i₂ : measurable_space β]
(h : α = β)
(hi : i₁ == i₂) :
α ≃ᵐ β
Equal measurable spaces are equivalent.
Equations
- measurable_equiv.cast h hi = {to_equiv := equiv.cast h, measurable_to_fun := _, measurable_inv_fun := _}
@[protected]
theorem
measurable_equiv.measurable_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{f : β → γ}
(e : α ≃ᵐ β) :
measurable (f ∘ ⇑e) ↔ measurable f
def
measurable_equiv.of_unique_of_unique
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[measurable_space β]
[unique α]
[unique β] :
α ≃ᵐ β
Any two types with unique elements are measurably equivalent.
Equations
- measurable_equiv.of_unique_of_unique α β = {to_equiv := equiv.equiv_of_unique α β _inst_8, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.prod_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
[measurable_space δ]
(ab : α ≃ᵐ β)
(cd : γ ≃ᵐ δ) :
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_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β] :
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.prod_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ] :
Products of measurable spaces are associative.
Equations
- measurable_equiv.prod_assoc = {to_equiv := equiv.prod_assoc α β γ, measurable_to_fun := _, measurable_inv_fun := _}
def
measurable_equiv.sum_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
[measurable_space δ]
(ab : α ≃ᵐ β)
(cd : γ ≃ᵐ δ) :
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_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(s : set α)
(t : set β) :
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.range_inl
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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 β γ δ))
def
measurable_equiv.Pi_congr_right
{δ' : Type u_5}
{π : δ' → Type u_7}
{π' : δ' → Type u_8}
[Π (x : δ'), measurable_space (π x)]
[Π (x : δ'), measurable_space (π' x)]
(e : Π (a : δ'), π a ≃ᵐ π' a) :
A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence
between Π a, β₁ a and Π a, β₂ a.
Equations
- measurable_equiv.Pi_congr_right e = {to_equiv := equiv.Pi_congr_right (λ (a : δ'), (e a).to_equiv), measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
theorem
measurable_equiv.pi_measurable_equiv_tprod_apply
{δ' : Type u_5}
{π : δ' → Type u_7}
[Π (x : δ'), measurable_space (π x)]
[decidable_eq δ']
{l : list δ'}
(hnd : l.nodup)
(h : ∀ (i : δ'), i ∈ l) :
def
measurable_equiv.pi_measurable_equiv_tprod
{δ' : Type u_5}
{π : δ' → Type u_7}
[Π (x : δ'), measurable_space (π x)]
[decidable_eq δ']
{l : list δ'}
(hnd : l.nodup)
(h : ∀ (i : δ'), i ∈ l) :
(Π (i : δ'), π i) ≃ᵐ list.tprod π l
Pi-types are measurably equivalent to iterated products.
Equations
- measurable_equiv.pi_measurable_equiv_tprod hnd h = {to_equiv := list.tprod.pi_equiv_tprod hnd h, measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
theorem
measurable_equiv.pi_measurable_equiv_tprod_to_equiv
{δ' : Type u_5}
{π : δ' → Type u_7}
[Π (x : δ'), measurable_space (π x)]
[decidable_eq δ']
{l : list δ'}
(hnd : l.nodup)
(h : ∀ (i : δ'), i ∈ l) :
@[simp]
theorem
measurable_equiv.pi_measurable_equiv_tprod_symm_apply
{δ' : Type u_5}
{π : δ' → Type u_7}
[Π (x : δ'), measurable_space (π x)]
[decidable_eq δ']
{l : list δ'}
(hnd : l.nodup)
(h : ∀ (i : δ'), i ∈ l) :
If α has a unique term, then the type of function α → β is measurably equivalent to β.
Equations
- measurable_equiv.fun_unique α β = {to_equiv := equiv.fun_unique α β _inst_7, measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
theorem
measurable_equiv.fun_unique_to_equiv
(α : Type u_1)
(β : Type u_2)
[unique α]
[measurable_space β] :
(measurable_equiv.fun_unique α β).to_equiv = equiv.fun_unique α β
@[simp]
theorem
measurable_equiv.fun_unique_apply
(α : Type u_1)
(β : Type u_2)
[unique α]
[measurable_space β] :
@[simp]
theorem
measurable_equiv.fun_unique_symm_apply
(α : Type u_1)
(β : Type u_2)
[unique α]
[measurable_space β] :
⇑((measurable_equiv.fun_unique α β).symm) = λ (x : β) (b : α), x
@[simp]
theorem
measurable_equiv.pi_fin_two_symm_apply
(α : fin 2 → Type u_1)
[Π (i : fin 2), measurable_space (α i)] :
⇑((measurable_equiv.pi_fin_two α).symm) = λ (p : α 0 × α 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
@[simp]
theorem
measurable_equiv.pi_fin_two_apply
(α : fin 2 → Type u_1)
[Π (i : fin 2), measurable_space (α i)] :
⇑(measurable_equiv.pi_fin_two α) = λ (f : Π (i : fin 2), α i), (f 0, f 1)
@[simp]
theorem
measurable_equiv.pi_fin_two_to_equiv
(α : fin 2 → Type u_1)
[Π (i : fin 2), measurable_space (α i)] :
The space Π i : fin 2, α i is measurably equivalent to α 0 × α 1.
Equations
- measurable_equiv.pi_fin_two α = {to_equiv := pi_fin_two_equiv α, measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
theorem
measurable_equiv.fin_two_arrow_apply
{α : Type u_1}
[measurable_space α] :
⇑measurable_equiv.fin_two_arrow = λ (f : fin 2 → α), (f 0, f 1)
@[simp]
@[simp]
@[simp]
theorem
measurable_equiv.fin_two_arrow_symm_apply
{α : Type u_1}
[measurable_space α] :
⇑(measurable_equiv.fin_two_arrow.symm) = λ (p : α × α), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
The space fin 2 → α is measurably equivalent to α × α.
Equations
- measurable_equiv.fin_two_arrow = measurable_equiv.pi_fin_two (λ (_x : fin 2), α)
def
measurable_equiv.pi_fin_succ_above_equiv
{n : ℕ}
(α : fin (n + 1) → Type u_1)
[Π (i : fin (n + 1)), measurable_space (α i)]
(i : fin (n + 1)) :
Measurable equivalence between Π j : fin (n + 1), α j and
α i × Π j : fin n, α (fin.succ_above i j).
Equations
- measurable_equiv.pi_fin_succ_above_equiv α i = {to_equiv := equiv.pi_fin_succ_above_equiv α i, measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
@[simp]
theorem
measurable_equiv.pi_fin_succ_above_equiv_symm_apply
{n : ℕ}
(α : fin (n + 1) → Type u_1)
[Π (i : fin (n + 1)), measurable_space (α i)]
(i : fin (n + 1)) :
⇑((measurable_equiv.pi_fin_succ_above_equiv α i).symm) = λ (f : α i × Π (j : fin n), α (⇑(i.succ_above) j)), i.insert_nth f.fst f.snd
def
measurable_equiv.pi_equiv_pi_subtype_prod
{δ' : Type u_5}
(π : δ' → Type u_7)
[Π (x : δ'), measurable_space (π x)]
(p : δ' → Prop)
[decidable_pred p] :
Measurable equivalence between (dependent) functions on a type and pairs of functions on
{i // p i} and {i // ¬p i}. See also equiv.pi_equiv_pi_subtype_prod.
Equations
- measurable_equiv.pi_equiv_pi_subtype_prod π p = {to_equiv := equiv.pi_equiv_pi_subtype_prod p π (λ (a : δ'), _inst_7 a), measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
theorem
measurable_equiv.pi_equiv_pi_subtype_prod_symm_apply
{δ' : Type u_5}
(π : δ' → Type u_7)
[Π (x : δ'), measurable_space (π x)]
(p : δ' → Prop)
[decidable_pred p] :
@[simp]
theorem
measurable_equiv.pi_equiv_pi_subtype_prod_to_equiv
{δ' : Type u_5}
(π : δ' → Type u_7)
[Π (x : δ'), measurable_space (π x)]
(p : δ' → Prop)
[decidable_pred p] :
@[simp]
theorem
measurable_equiv.pi_equiv_pi_subtype_prod_apply
{δ' : Type u_5}
(π : δ' → Type u_7)
[Π (x : δ'), measurable_space (π x)]
(p : δ' → Prop)
[decidable_pred p] :
def
measurable_equiv.sum_compl
{α : Type u_1}
[measurable_space α]
{s : set α}
[decidable_pred s]
(hs : measurable_set s) :
If s is a measurable set in a measurable space, that space is equivalent
to the sum of s and sᶜ.
Equations
- measurable_equiv.sum_compl hs = {to_equiv := equiv.sum_compl s (λ (a : α), _inst_7 a), measurable_to_fun := _, measurable_inv_fun := _}
@[simp]
theorem
measurable_equiv.of_involutive_to_equiv
{α : Type u_1}
[measurable_space α]
(f : α → α)
(hf : function.involutive f)
(hf' : measurable f) :
(measurable_equiv.of_involutive f hf hf').to_equiv = function.involutive.to_perm f hf
def
measurable_equiv.of_involutive
{α : Type u_1}
[measurable_space α]
(f : α → α)
(hf : function.involutive f)
(hf' : measurable f) :
α ≃ᵐ α
Convert a measurable involutive function f to a measurable permutation with
to_fun = inv_fun = f. See also function.involutive.to_perm.
Equations
- measurable_equiv.of_involutive f hf hf' = {to_equiv := {to_fun := (function.involutive.to_perm f hf).to_fun, inv_fun := (function.involutive.to_perm f hf).inv_fun, left_inv := _, right_inv := _}, measurable_to_fun := hf', measurable_inv_fun := hf'}
@[simp]
theorem
measurable_equiv.of_involutive_apply
{α : Type u_1}
[measurable_space α]
(f : α → α)
(hf : function.involutive f)
(hf' : measurable f)
(a : α) :
⇑(measurable_equiv.of_involutive f hf hf') a = f a
@[simp]
theorem
measurable_equiv.of_involutive_symm
{α : Type u_1}
[measurable_space α]
(f : α → α)
(hf : function.involutive f)
(hf' : measurable f) :
(measurable_equiv.of_involutive f hf hf').symm = measurable_equiv.of_involutive f hf hf'
@[simp]
theorem
measurable_embedding.comap_eq
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
(hf : measurable_embedding f) :
measurable_space.comap f _inst_2 = _inst_1
theorem
measurable_embedding.iff_comap_eq
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β} :
measurable_embedding f ↔ function.injective f ∧ measurable_space.comap f _inst_2 = _inst_1 ∧ measurable_set (set.range f)
noncomputable
def
measurable_embedding.equiv_image
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
(s : set α)
(hf : measurable_embedding f) :
A set is equivalent to its image under a function f as measurable spaces,
if f is a measurable embedding
Equations
- measurable_embedding.equiv_image s hf = {to_equiv := equiv.set.image f s _, measurable_to_fun := _, measurable_inv_fun := _}
noncomputable
def
measurable_embedding.equiv_range
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
(hf : measurable_embedding f) :
The domain of f is equivalent to its range as measurable spaces,
if f is a measurable embedding
Equations
- hf.equiv_range = (measurable_equiv.set.univ α).symm.trans ((measurable_embedding.equiv_image set.univ hf).trans (measurable_equiv.cast measurable_embedding.equiv_range._proof_1 measurable_embedding.equiv_range._proof_2))
theorem
measurable_embedding.of_measurable_inverse_on_range
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
{g : ↥(set.range f) → α}
(hf₁ : measurable f)
(hf₂ : measurable_set (set.range f))
(hg : measurable g)
(H : function.left_inverse g (set.range_factorization f)) :
theorem
measurable_embedding.of_measurable_inverse
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
{g : β → α}
(hf₁ : measurable f)
(hf₂ : measurable_set (set.range f))
(hg : measurable g)
(H : function.left_inverse g f) :
noncomputable
def
measurable_embedding.schroeder_bernstein
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
{g : β → α}
(hf : measurable_embedding f)
(hg : measurable_embedding g) :
α ≃ᵐ β
The **measurable Schröder-Bernstein Theorem**: Given measurable embeddingsα → βandβ → α, we can find a measurable equivalenceα ≃ᵐ β`.
Equations
- hf.schroeder_bernstein hg = let F : set α → set α := λ (A : set α), (g '' (f '' A)ᶜ)ᶜ in (let X : ℕ → set α := λ (n : ℕ), F^[n] set.univ in ⟨set.Inter X, _⟩).cases_on (λ (A : set α) (this_snd : measurable_set A ∧ F A = A), this_snd.dcases_on (λ (Ameas : measurable_set A) (Afp : F A = A), let B : set β := f '' A in (measurable_equiv.sum_compl Ameas).symm.trans (((measurable_embedding.equiv_image A hf).sum_congr (_.mpr (measurable_embedding.equiv_image Bᶜ hg).symm)).trans (measurable_equiv.sum_compl _))))
theorem
measurable_space.comap_compl
{α : Type u_1}
{β : Type u_2}
{m' : measurable_space β}
[boolean_algebra β]
(h : measurable has_compl.compl)
(f : α → β) :
measurable_space.comap (λ (a : α), (f a)ᶜ) infer_instance = measurable_space.comap f infer_instance
@[simp]
theorem
measurable_space.comap_not
{α : Type u_1}
(p : α → Prop) :
measurable_space.comap (λ (a : α), ¬p a) infer_instance = measurable_space.comap p infer_instance
@[class]
We say a measurable space is countably generated if can be generated by a countable set of sets.
Instances of this typeclass
theorem
measurable_space.measurable_injection_nat_bool_of_countably_generated
(α : Type u_1)
[measurable_space α]
[h : measurable_space.countably_generated α]
[measurable_singleton_class α] :
∃ (f : α → ℕ → bool), measurable f ∧ function.injective f
If a measurable space is countably generated, it admits a measurable injection
into the Cantor space ℕ → bool (equipped with the product sigma algebra).
@[class]
- exists_measurable_subset : ∀ ⦃s : set α⦄, s ∈ f → (∃ (t : set α) (H : t ∈ f), measurable_set t ∧ t ⊆ s)
A filter f is measurably generates if each s ∈ f includes a measurable t ∈ f.
Instances of this typeclass
- 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
- nhds_within_Icc_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
- nhds_within_uIcc_is_measurably_generated
@[protected, instance]
@[protected, instance]
theorem
filter.eventually.exists_measurable_mem
{α : Type u_1}
[measurable_space α]
{f : filter α}
[f.is_measurably_generated]
{p : α → Prop}
(h : ∀ᶠ (x : α) in f, p x) :
theorem
filter.eventually.exists_measurable_mem_of_small_sets
{α : Type u_1}
[measurable_space α]
{f : filter α}
[f.is_measurably_generated]
{p : set α → Prop}
(h : ∀ᶠ (s : set α) in f.small_sets, p s) :
@[protected, instance]
def
filter.inf_is_measurably_generated
{α : Type u_1}
[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_1}
[measurable_space α]
{s : set α} :
theorem
measurable_set.principal_is_measurably_generated
{α : Type u_1}
[measurable_space α]
{s : set α} :
Alias of the reverse direction of filter.principal_is_measurably_generated_iff.
@[protected, instance]
def
filter.infi_is_measurably_generated
{α : Type u_1}
{ι : Sort u_6}
[measurable_space α]
{f : ι → filter α}
[∀ (i : ι), (f i).is_measurably_generated] :
(⨅ (i : ι), f i).is_measurably_generated
We say that a collection of sets is countably spanning if a countable subset spans the
whole type. This is a useful condition in various parts of measure theory. For example, it is
a needed condition to show that the product of two collections generate the product sigma algebra,
see generate_from_prod_eq.
theorem
is_countably_spanning_measurable_set
{α : Type u_1}
[measurable_space α] :
is_countably_spanning {s : set α | measurable_set s}
Typeclasses on subtype measurable_set #
@[protected, instance]
Equations
- measurable_set.subtype.has_mem = {mem := λ (a : α) (s : subtype measurable_set), a ∈ ↑s}
@[simp]
theorem
measurable_set.mem_coe
{α : Type u_1}
[measurable_space α]
(a : α)
(s : subtype measurable_set) :
@[protected, instance]
@[protected, instance]
def
measurable_set.subtype.has_insert
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α] :
Equations
- measurable_set.subtype.has_insert = {insert := λ (a : α) (s : subtype measurable_set), ⟨has_insert.insert a ↑s, _⟩}
@[simp]
theorem
measurable_set.coe_insert
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(a : α)
(s : subtype measurable_set) :
↑(has_insert.insert a s) = has_insert.insert a ↑s
@[protected, instance]
Equations
- measurable_set.subtype.has_compl = {compl := λ (x : subtype measurable_set), ⟨(↑x)ᶜ, _⟩}
@[simp]
@[protected, instance]
Equations
- measurable_set.subtype.has_union = {union := λ (x y : subtype measurable_set), ⟨↑x ∪ ↑y, _⟩}
@[simp]
theorem
measurable_set.coe_union
{α : Type u_1}
[measurable_space α]
(s t : subtype measurable_set) :
@[protected, instance]
Equations
- measurable_set.subtype.has_inter = {inter := λ (x y : subtype measurable_set), ⟨↑x ∩ ↑y, _⟩}
@[simp]
theorem
measurable_set.coe_inter
{α : Type u_1}
[measurable_space α]
(s t : subtype measurable_set) :
@[protected, instance]
Equations
- measurable_set.subtype.has_sdiff = {sdiff := λ (x y : subtype measurable_set), ⟨↑x \ ↑y, _⟩}
@[simp]
theorem
measurable_set.coe_sdiff
{α : Type u_1}
[measurable_space α]
(s t : subtype measurable_set) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- measurable_set.subtype.partial_order = partial_order.lift coe measurable_set.subtype.partial_order._proof_1
@[protected, instance]
Equations
- measurable_set.subtype.distrib_lattice = {sup := has_union.union measurable_set.subtype.has_union, le := partial_order.le measurable_set.subtype.partial_order, lt := partial_order.lt measurable_set.subtype.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter measurable_set.subtype.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
@[protected, instance]
@[protected, instance]
Equations
- measurable_set.subtype.boolean_algebra = {sup := distrib_lattice.sup measurable_set.subtype.distrib_lattice, le := distrib_lattice.le measurable_set.subtype.distrib_lattice, lt := distrib_lattice.lt measurable_set.subtype.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf measurable_set.subtype.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := has_compl.compl measurable_set.subtype.has_compl, sdiff := has_sdiff.sdiff measurable_set.subtype.has_sdiff, himp := λ (x y : subtype measurable_set), distrib_lattice.sup y xᶜ, top := bounded_order.top measurable_set.subtype.bounded_order, bot := bounded_order.bot measurable_set.subtype.bounded_order, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}
@[measurability]
theorem
measurable_set.measurable_set_blimsup
{α : Type u_1}
[measurable_space α]
{s : ℕ → set α}
{p : ℕ → Prop}
(h : ∀ (n : ℕ), p n → measurable_set (s n)) :
@[measurability]
theorem
measurable_set.measurable_set_bliminf
{α : Type u_1}
[measurable_space α]
{s : ℕ → set α}
{p : ℕ → Prop}
(h : ∀ (n : ℕ), p n → measurable_set (s n)) :
@[measurability]
theorem
measurable_set.measurable_set_limsup
{α : Type u_1}
[measurable_space α]
{s : ℕ → set α}
(hs : ∀ (n : ℕ), measurable_set (s n)) :
@[measurability]
theorem
measurable_set.measurable_set_liminf
{α : Type u_1}
[measurable_space α]
{s : ℕ → set α}
(hs : ∀ (n : ℕ), measurable_set (s n)) :