mathlib documentation

measure_theory.measurable_space

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.

Notation

Implementation notes

Measurability of a function f : α → β between measurable spaces is defined in terms of the Galois connection induced by f.

References

Tags

measurable space, σ-algebra, measurable function, measurable equivalence, dynkin system, π-λ theorem, π-system

@[instance]

Equations
def is_measurable {α : Type u_1} [measurable_space α] :
set α → Prop

is_measurable s means that s is measurable (in the ambient measure space on α)

Equations
@[simp]
theorem is_measurable.empty {α : Type u_1} [measurable_space α] :

theorem is_measurable.compl {α : Type u_1} {s : set α} [measurable_space α] :

theorem is_measurable.of_compl {α : Type u_1} {s : set α} [measurable_space α] (h : is_measurable s) :

@[simp]
theorem is_measurable.compl_iff {α : Type u_1} {s : set α} [measurable_space α] :

@[simp]
theorem is_measurable.univ {α : Type u_1} [measurable_space α] :

theorem subsingleton.is_measurable {α : Type u_1} [measurable_space α] [subsingleton α] {s : set α} :

theorem is_measurable.congr {α : Type u_1} [measurable_space α] {s t : set α} (hs : is_measurable s) (h : s = t) :

theorem is_measurable.bUnion_decode2 {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [measurable_space α] [encodable β] ⦃f : β → set α (h : ∀ (b : β), is_measurable (f b)) :
is_measurable (⋃ (b : β), f b)

theorem is_measurable.bUnion {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.countable) (h : ∀ (b : β), b sis_measurable (f b)) :
is_measurable (⋃ (b : β) (H : b s), f b)

theorem set.finite.is_measurable_bUnion {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.finite) (h : ∀ (b : β), b sis_measurable (f b)) :
is_measurable (⋃ (b : β) (H : b s), f b)

theorem finset.is_measurable_bUnion {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} (s : finset β) (h : ∀ (b : β), b sis_measurable (f b)) :
is_measurable (⋃ (b : β) (H : b s), f b)

theorem is_measurable.sUnion {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.countable) (h : ∀ (t : set α), t sis_measurable t) :

theorem set.finite.is_measurable_sUnion {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.finite) (h : ∀ (t : set α), t sis_measurable t) :

theorem is_measurable.Union_Prop {α : Type u_1} [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_1} {β : Type u_2} [measurable_space α] [encodable β] {f : β → set α} (h : ∀ (b : β), is_measurable (f b)) :
is_measurable (⋂ (b : β), f b)

theorem is_measurable.Union_fintype {α : Type u_1} {β : Type u_2} [measurable_space α] [fintype β] {f : β → set α} (h : ∀ (b : β), is_measurable (f b)) :
is_measurable (⋃ (b : β), f b)

theorem is_measurable.Inter_fintype {α : Type u_1} {β : Type u_2} [measurable_space α] [fintype β] {f : β → set α} (h : ∀ (b : β), is_measurable (f b)) :
is_measurable (⋂ (b : β), f b)

theorem is_measurable.bInter {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.countable) (h : ∀ (b : β), b sis_measurable (f b)) :
is_measurable (⋂ (b : β) (H : b s), f b)

theorem set.finite.is_measurable_bInter {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.finite) (h : ∀ (b : β), b sis_measurable (f b)) :
is_measurable (⋂ (b : β) (H : b s), f b)

theorem finset.is_measurable_bInter {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} (s : finset β) (h : ∀ (b : β), b sis_measurable (f b)) :
is_measurable (⋂ (b : β) (H : b s), f b)

theorem is_measurable.sInter {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.countable) (h : ∀ (t : set α), t sis_measurable t) :

theorem set.finite.is_measurable_sInter {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.finite) (h : ∀ (t : set α), t sis_measurable t) :

theorem is_measurable.Inter_Prop {α : Type u_1} [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_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
is_measurable (s₁ s₂)

@[simp]
theorem is_measurable.inter {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
is_measurable (s₁ s₂)

@[simp]
theorem is_measurable.diff {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
is_measurable (s₁ \ s₂)

@[simp]
theorem is_measurable.disjointed {α : Type u_1} [measurable_space α] {f : set α} (h : ∀ (i : ), is_measurable (f i)) (n : ) :

@[simp]
theorem is_measurable.const {α : Type u_1} [measurable_space α] (p : Prop) :
is_measurable {a : α | p}

theorem nonempty_measurable_superset {α : Type u_1} [measurable_space α] (s : set α) :

Every set has a measurable superset. Declare this as local instance as needed.

@[ext]
theorem measurable_space.ext {α : Type u_1} {m₁ m₂ : measurable_space α} :
(∀ (s : set α), m₁.is_measurable' s m₂.is_measurable' s)m₁ = m₂

@[ext]
theorem measurable_space.ext_iff {α : Type u_1} {m₁ m₂ : measurable_space α} :
m₁ = m₂ ∀ (s : set α), m₁.is_measurable' s m₂.is_measurable' s

@[class]
structure measurable_singleton_class (α : Type u_7) [measurable_space α] :
Prop

A typeclass mixin for measurable_spaces such that each singleton is measurable.

Instances
theorem is_measurable_eq {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {a : α} :
is_measurable {x : α | x = a}

theorem is_measurable.insert {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {s : set α} (hs : is_measurable s) (a : α) :

@[simp]
theorem is_measurable_insert {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {a : α} {s : set α} :

theorem set.finite.is_measurable {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {s : set α} (hs : s.finite) :

@[instance]

Equations
inductive measurable_space.generate_measurable {α : Type u_1} (s : set (set α)) :
set α → Prop

The smallest σ-algebra containing a collection s of basic sets

def measurable_space.generate_from {α : Type u_1} (s : set (set α)) :

Construct the smallest measure space containing a collection of basic sets

Equations
theorem measurable_space.is_measurable_generate_from {α : Type u_1} {s : set (set α)} {t : set α} (ht : t s) :

theorem measurable_space.generate_from_le {α : Type u_1} {s : set (set α)} {m : measurable_space α} (h : ∀ (t : set α), t sm.is_measurable' t) :

def measurable_space.mk_of_closure {α : Type u_1} (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

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
theorem measurable_space.is_measurable_bot_iff {α : Type u_1} {s : set α} :

@[simp]
theorem measurable_space.is_measurable_top {α : Type u_1} {s : set α} :

@[simp]
theorem measurable_space.is_measurable_inf {α : Type u_1} {m₁ m₂ : measurable_space α} {s : set α} :

@[simp]
theorem measurable_space.is_measurable_Inf {α : Type u_1} {ms : set (measurable_space α)} {s : set α} :

@[simp]
theorem measurable_space.is_measurable_infi {α : Type u_1} {ι : Sort u_2} {m : ι → measurable_space α} {s : set α} :
is_measurable s ∀ (i : ι), is_measurable s

theorem measurable_space.is_measurable_Sup {α : Type u_1} {ms : set (measurable_space α)} {s : set α} :

theorem measurable_space.is_measurable_supr {α : Type u_1} {ι : Sort u_2} {m : ι → measurable_space α} {s : set α} :

def measurable_space.map {α : Type u_1} {β : Type u_2} (f : α → β) (m : measurable_space α) :

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
@[simp]
theorem measurable_space.map_id {α : Type u_1} {m : measurable_space α} :

@[simp]
theorem measurable_space.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {f : α → β} {g : β → γ} :

def measurable_space.comap {α : Type u_1} {β : Type u_2} (f : α → β) (m : measurable_space β) :

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
@[simp]
theorem measurable_space.comap_id {α : Type u_1} {m : measurable_space α} :

@[simp]
theorem measurable_space.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {f : β → α} {g : γ → β} :

theorem measurable_space.comap_le_iff_le_map {α : Type u_1} {β : Type u_2} {m : measurable_space α} {m' : measurable_space β} {f : α → β} :

theorem measurable_space.gc_comap_map {α : Type u_1} {β : Type u_2} (f : α → β) :

theorem measurable_space.map_mono {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {f : α → β} (h : m₁ m₂) :

theorem measurable_space.monotone_map {α : Type u_1} {β : Type u_2} {f : α → β} :

theorem measurable_space.comap_mono {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {g : β → α} (h : m₁ m₂) :

theorem measurable_space.monotone_comap {α : Type u_1} {β : Type u_2} {g : β → α} :

@[simp]
theorem measurable_space.comap_bot {α : Type u_1} {β : Type u_2} {g : β → α} :

@[simp]
theorem measurable_space.comap_sup {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {g : β → α} :

@[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]
theorem measurable_space.map_top {α : Type u_1} {β : Type u_2} {f : α → β} :

@[simp]
theorem measurable_space.map_inf {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {f : α → β} :

@[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 : α → β} :

theorem measurable_space.le_map_comap {α : Type u_1} {β : Type u_2} {m : measurable_space α} {g : β → α} :

def measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (f : α → β) :
Prop

A function f between measurable spaces is measurable if the preimage of every measurable set is measurable.

Equations
theorem measurable_iff_le_map {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :

theorem measurable.le_map {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :

Alias of measurable_iff_le_map.

theorem measurable.of_le_map {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :

Alias of measurable_iff_le_map.

theorem measurable_iff_comap_le {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :

theorem measurable.comap_le {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :

Alias of measurable_iff_comap_le.

theorem measurable.of_comap_le {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :

Alias 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) :

theorem measurable_from_top {α : Type u_1} {β : Type u_2} [measurable_space β] {f : α → β} :

theorem measurable_generate_from {α : Type u_1} {β : Type u_2} [measurable_space α] {s : set (set β)} {f : α → β} (h : ∀ (t : set β), t sis_measurable (f ⁻¹' t)) :

theorem measurable_id {α : Type u_1} [measurable_space α] :

theorem measurable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) :

theorem subsingleton.measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [subsingleton α] {f : α → β} :

theorem measurable.piecewise {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {s : set α} {_x : decidable_pred s} {f g : α → β} (hs : is_measurable s) (hf : measurable f) (hg : measurable g) :

theorem measurable.ite {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {p : α → Prop} {_x : decidable_pred p} {f g : α → β} (hp : is_measurable {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 (is_measurable_singleton 0) measurable_const measurable_const, but replacing measurable.ite by measurable.piecewise in that example proof does not work.

@[simp]
theorem measurable_const {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {a : α} :
measurable (λ (b : β), a)

theorem measurable.indicator {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [has_zero β] {s : set α} {f : α → β} (hf : measurable f) (hs : is_measurable s) :

theorem measurable_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [has_zero α] :

theorem measurable_one {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [has_one α] :

theorem measurable_of_not_nonempty {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (h : ¬nonempty α) (f : α → β) :

theorem measurable_to_encodable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [encodable α] {f : β → α} (h : ∀ (y : β), is_measurable (f ⁻¹' {f y})) :

theorem measurable_unit {α : Type u_1} [measurable_space α] (f : unit → α) :

theorem measurable_from_nat {α : Type u_1} [measurable_space α] {f : → α} :

theorem measurable_to_nat {α : Type u_1} [measurable_space α] {f : α → } :
(∀ (y : α), is_measurable (f ⁻¹' {f y}))measurable f

theorem measurable_find_greatest' {α : Type u_1} [measurable_space α] {p : α → → Prop} {N : } (hN : ∀ (k : ), k Nis_measurable {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} {N : } (hN : ∀ (k : ), k Nis_measurable {x : α | p x k}) :
measurable (λ (x : α), nat.find_greatest (p x) N)

theorem measurable_find {α : Type u_1} [measurable_space α] {p : α → → Prop} (hp : ∀ (x : α), ∃ (N : ), p x N) (hm : ∀ (k : ), is_measurable {x : α | p x k}) :
measurable (λ (x : α), nat.find _)

@[instance]
def subtype.measurable_space {α : Type u_1} {p : α → Prop} [m : measurable_space α] :

Equations
theorem measurable_subtype_coe {α : Type u_1} [measurable_space α] {p : α → Prop} :

theorem measurable.subtype_coe {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {p : β → Prop} {f : α → subtype p} (hf : measurable f) :
measurable (λ (a : α), (f a))

theorem measurable.subtype_mk {α : Type u_1} {β : Type u_2} [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_1} [measurable_space α] {s : set α} {t : set s} (hs : is_measurable s) :

theorem measurable_of_measurable_union_cover {α : Type u_1} {β : Type u_2} [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_1} {β : Type u_2} [measurable_space α] [measurable_space β] [measurable_singleton_class α] {f : α → β} (a : α) (hf : measurable (set.restrict f {x : α | x a})) :

@[instance]
def prod.measurable_space {α : Type u_1} {β : Type u_2} [m₁ : measurable_space α] [m₂ : measurable_space β] :

Equations
theorem measurable_fst {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

theorem measurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β × γ} (hf : measurable f) :
measurable (λ (a : α), (f a).fst)

theorem measurable_snd {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

theorem measurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β × γ} (hf : measurable f) :
measurable (λ (a : α), (f a).snd)

theorem measurable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β × γ} (hf₁ : measurable (λ (a : α), (f a).fst)) (hf₂ : measurable (λ (a : α), (f a).snd)) :

theorem measurable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} {γ : Type u_3} [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_1} {β : Type u_2} [measurable_space α] [measurable_space β] {x : α} :

theorem measurable_prod_mk_right {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {y : β} :
measurable (λ (x : α), (x, y))

theorem measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β → γ} (hf : measurable (function.uncurry f)) {x : α} :

theorem measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β → γ} (hf : measurable (function.uncurry f)) {y : β} :
measurable (λ (x : α), f x y)

theorem measurable_swap {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

theorem measurable_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α × β → γ} :

theorem is_measurable.prod {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {s : set α} {t : set β} (hs : is_measurable s) (ht : is_measurable t) :

theorem is_measurable_prod_of_nonempty {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {s : set α} {t : set β} (h : (s.prod t).nonempty) :

theorem is_measurable_prod {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {s : set α} {t : set β} :

theorem is_measurable_swap_iff {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {s : set × β)} :

@[instance]
def measurable_space.pi {δ : Type u_4} {π : δ → Type u_7} [m : Π (a : δ), measurable_space («π» a)] :
measurable_space (Π (a : δ), «π» a)

Equations
theorem measurable_pi_iff {α : Type u_1} {δ : Type u_4} [measurable_space α] {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] {g : α → Π (a : δ), «π» a} :
measurable g ∀ (a : δ), measurable (λ (x : α), g x a)

theorem measurable_pi_apply {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] (a : δ) :
measurable (λ (f : Π (a : δ), «π» a), f a)

theorem measurable.eval {α : Type u_1} {δ : Type u_4} [measurable_space α] {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] {a : δ} {g : α → Π (a : δ), «π» a} (hg : measurable g) :
measurable (λ (x : α), g x a)

theorem measurable_pi_lambda {α : Type u_1} {δ : Type u_4} [measurable_space α] {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] (f : α → Π (a : δ), «π» a) (hf : ∀ (a : δ), measurable (λ (c : α), f c a)) :

theorem measurable_update {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] (f : Π (a : δ), «π» a) {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.

theorem is_measurable.pi {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] {s : set δ} {t : Π (i : δ), set («π» i)} (hs : s.countable) (ht : ∀ (i : δ), i sis_measurable (t i)) :

theorem is_measurable.pi_univ {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] [encodable δ] {t : Π (i : δ), set («π» i)} (ht : ∀ (i : δ), is_measurable (t i)) :

theorem is_measurable_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) :
is_measurable (s.pi t) ∀ (i : δ), i sis_measurable (t i)

theorem is_measurable_pi {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] {s : set δ} {t : Π (i : δ), set («π» i)} (hs : s.countable) :
is_measurable (s.pi t) (∀ (i : δ), i sis_measurable (t i)) s.pi t =

theorem is_measurable.pi_fintype {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space («π» a)] [fintype δ] {s : set δ} {t : Π (i : δ), set («π» i)} (ht : ∀ (i : δ), i sis_measurable (t i)) :

@[instance]
def tprod.measurable_space {δ : Type u_4} (π : δ → Type u_1) [Π (x : δ), measurable_space («π» x)] (l : list δ) :

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)] {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)] {l : list δ} (h : ∀ (i : δ), i l) :

theorem is_measurable.tprod {δ : Type u_4} {π : δ → Type u_7} [Π (x : δ), measurable_space («π» x)] (l : list δ) {s : Π (i : δ), set («π» i)} (hs : ∀ (i : δ), is_measurable (s i)) :

@[instance]
def sum.measurable_space {α : Type u_1} {β : Type u_2} [m₁ : measurable_space α] [m₂ : measurable_space β] :

Equations
theorem measurable_inl {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

theorem measurable_inr {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

theorem measurable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α β → γ} (hl : measurable (f sum.inl)) (hr : measurable (f sum.inr)) :

theorem measurable.sum_elim {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → γ} {g : β → γ} (hf : measurable f) (hg : measurable g) :

theorem is_measurable.inl_image {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {s : set α} (hs : is_measurable s) :

theorem is_measurable_range_inl {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

theorem is_measurable_inr_image {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {s : set β} (hs : is_measurable s) :

theorem is_measurable_range_inr {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

@[instance]
def sigma.measurable_space {α : Type u_1} {β : α → Type u_2} [m : Π (a : α), measurable_space (β a)] :

Equations
structure measurable_equiv (α : Type u_7) (β : Type u_8) [measurable_space α] [measurable_space β] :
Type (max u_7 u_8)

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
theorem measurable_equiv.coe_eq {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (e : α ≃ᵐ β) :

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)) :

def measurable_equiv.refl (α : Type u_1) [measurable_space α] :
α ≃ᵐ α

Any measurable space is equivalent to itself.

Equations
@[instance]
def measurable_equiv.inhabited {α : Type u_1} [measurable_space α] :

Equations
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
@[simp]
theorem measurable_equiv.trans_to_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :

def measurable_equiv.symm {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (ab : α ≃ᵐ β) :
β ≃ᵐ α

The inverse of an equivalence between measurable spaces.

Equations
@[simp]
theorem measurable_equiv.symm_to_equiv {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (ab : α ≃ᵐ β) :

@[simp]
theorem measurable_equiv.coe_symm_mk {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (e : α β) (h1 : measurable e) (h2 : measurable (e.symm)) :

@[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 : α ≃ᵐ β) :

def measurable_equiv.cast {α β : Type u_1} [i₁ : measurable_space α] [i₂ : measurable_space β] (h : α = β) (hi : i₁ == i₂) :
α ≃ᵐ β

Equal measurable spaces are equivalent.

Equations
theorem measurable_equiv.measurable_coe_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {f : β → γ} (e : α ≃ᵐ β) :

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
def measurable_equiv.prod_comm {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :
α × β ≃ᵐ β × α

Products of measurable spaces are symmetric.

Equations
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
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
def measurable_equiv.set.prod {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (s : set α) (t : set β) :

set.prod s t ≃ (s × t) as measurable spaces.

Equations

univ α ≃ α as measurable spaces.

Equations
def measurable_equiv.set.singleton {α : Type u_1} [measurable_space α] (a : α) :

{a} ≃ unit as measurable spaces.

Equations
def measurable_equiv.set.image {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (f : α → β) (s : set α) (hf : function.injective f) (hfm : measurable f) (hfi : ∀ (s : set α), is_measurable sis_measurable (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
def measurable_equiv.set.range {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (f : α → β) (hf : function.injective f) (hfm : measurable f) (hfi : ∀ (s : set α), is_measurable sis_measurable (f '' s)) :

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
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
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
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
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.

Equations
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
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 : δ'), «π» a) ≃ᵐ Π (a : δ'), π' a

A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence between Π a, β₁ a and Π a, β₂ a.

Equations
def measurable_equiv.pi_measurable_equiv_tprod {δ' : Type u_5} {π : δ' → Type u_7} [Π (x : δ'), measurable_space («π» x)] {l : list δ'} (hnd : l.nodup) (h : ∀ (i : δ'), i l) :
(Π (i : δ'), «π» i) ≃ᵐ list.tprod «π» l

Pi-types are measurably equivalent to iterated products.

Equations
def is_pi_system {α : Type u_1} (C : set (set α)) :
Prop

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.

Equations
structure measurable_space.dynkin_system (α : Type u_7) :
Type u_7

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_1} {d₁ d₂ : measurable_space.dynkin_system α} :
(∀ (s : set α), d₁.has s d₂.has s)d₁ = d₂

theorem measurable_space.dynkin_system.has_Union {α : Type u_1} (d : measurable_space.dynkin_system α) {β : Type u_2} [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_union {α : Type u_1} (d : measurable_space.dynkin_system α) {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₁ s₂ ) :
d.has (s₁ s₂)

theorem measurable_space.dynkin_system.has_diff {α : Type u_1} (d : measurable_space.dynkin_system α) {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ s₁) :
d.has (s₁ \ s₂)

@[instance]

Equations

Every measurable space (σ-algebra) forms a Dynkin system

Equations
inductive measurable_space.dynkin_system.generate_has {α : Type u_1} (s : set (set α)) :
set α → Prop

The least Dynkin system containing a collection of basic sets. This inductive type gives the underlying collection of sets.

The least Dynkin system containing a collection of basic sets.

Equations
def measurable_space.dynkin_system.to_measurable_space {α : Type u_1} (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
theorem measurable_space.dynkin_system.of_measurable_space_to_measurable_space {α : Type u_1} (d : measurable_space.dynkin_system α) (h_inter : ∀ (s₁ s₂ : set α), d.has s₁d.has s₂d.has (s₁ s₂)) :

If s is in a Dynkin system d, we can form the new Dynkin system {s ∩ t | t ∈ d}.

Equations
theorem measurable_space.dynkin_system.generate_le {α : Type u_1} (d : measurable_space.dynkin_system α) {s : set (set α)} (h : ∀ (t : set α), t sd.has t) :

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_1} {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 sC t) (h_compl : ∀ (t : set α), is_measurable tC tC t) (h_union : ∀ (f : set α), pairwise (disjoint on f)(∀ (i : ), is_measurable (f i))(∀ (i : ), C (f i))C (⋃ (i : ), f i)) ⦃t : set α⦄ :
is_measurable tC t

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) :
∃ (s : set α) (H : s f), is_measurable s ∀ (x : α), x sp x

theorem filter.eventually.exists_measurable_mem_of_lift' {α : Type u_1} [measurable_space α] {f : filter α} [f.is_measurably_generated] {p : set α → Prop} (h : ∀ᶠ (s : set α) in f.lift' set.powerset, p s) :
∃ (s : set α) (H : s f), is_measurable s p s

Alias of principal_is_measurably_generated_iff.

@[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

def is_countably_spanning {α : Type u_1} (C : set (set α)) :
Prop

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.

Equations