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.

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, measurable function, dynkin system

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 α] :

@[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 α} :
is_measurable ss = tis_measurable 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 α :
(∀ (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 β} :
s.countable(∀ (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 β} :
s.finite(∀ (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 β) :
(∀ (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 α)} :
s.countable(∀ (t : set α), t sis_measurable t)is_measurable (⋃₀s)

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

theorem is_measurable.Union_Prop {α : Type u_1} [measurable_space α] {p : Prop} {f : p → set α} :
(∀ (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 α} :
(∀ (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 β} :
s.countable(∀ (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 β} :
s.finite(∀ (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 β) :
(∀ (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 α)} :
s.countable(∀ (t : set α), t sis_measurable t)is_measurable (⋂₀s)

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

theorem is_measurable.Inter_Prop {α : Type u_1} [measurable_space α] {p : Prop} {f : p → set α} :
(∀ (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 α} :
is_measurable s₁is_measurable s₂is_measurable (s₁ s₂)

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

@[simp]
theorem is_measurable.diff {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} :
is_measurable s₁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}

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

@[instance]

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

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

def measurable_space.generate_from {α : Type u_1} :

Construct the smallest measure space containing a collection of basic sets

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

def measurable_space.mk_of_closure {α : Type u_1} (g : set (set α)) :

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_supr {α : Type u_1} {ι : Sort u_2} {m : ι → measurable_space α} {s : set α} :

def measurable_space.map {α : Type u_1} {β : Type u_2} :
(α → β)measurable_space α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} :
(α → β)measurable_space β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 : α → β} :
m₁ m₂measurable_space.map f m₁ measurable_space.map f 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 : β → α} :

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 β] :
(α → β) → 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_iff_comap_le {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :

theorem measurable.mono {α : Type u_1} {β : Type u_2} {ma ma' : measurable_space α} {mb mb' : measurable_space β} {f : α → β} :
measurable fma ma'mb' mbmeasurable f

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 : α → β} :
(∀ (t : set β), t sis_measurable (f ⁻¹' t))measurable f

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

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

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

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_to_encodable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [encodable α] {f : β → α} :
(∀ (y : β), is_measurable (f ⁻¹' {f y}))measurable f

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 : } :
(∀ (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 : } :
(∀ (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) :
(∀ (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} :
measurable fmeasurable (λ (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} :

theorem measurable_of_measurable_union_cover {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {f : α → β} (s t : set α) :
is_measurable sis_measurable tset.univ s tmeasurable (λ (a : s), f a)measurable (λ (a : t), f a)measurable f

theorem measurable_of_measurable_on_compl_singleton {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [measurable_singleton_class α] {f : α → β} (a : α) :
measurable (set.restrict f {x : α | x a})measurable f

@[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 : α → β × γ} :
measurable fmeasurable (λ (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 : α → β × γ} :
measurable fmeasurable (λ (a : α), (f a).snd)

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

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 : α → γ} :
measurable fmeasurable gmeasurable (λ (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 β} :

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

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

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

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

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

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

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 β} :

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 : measurable_equiv α β) :

theorem measurable_equiv.measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (e : measurable_equiv α β) :

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

Any measurable space is equivalent to itself.

Equations
def measurable_equiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] :

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 : measurable_equiv α β) (bc : measurable_equiv β γ) :

def measurable_equiv.symm {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

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 : measurable_equiv α β) :

def measurable_equiv.cast {α β : Type u_1} [i₁ : measurable_space α] [i₂ : measurable_space β] :
α = βi₁ == i₂measurable_equiv α β

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 : measurable_equiv α β) :

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 δ] :
measurable_equiv α βmeasurable_equiv γ δmeasurable_equiv × γ) × δ)

Products of equivalent measurable spaces are equivalent.

Equations
def measurable_equiv.prod_comm {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :
measurable_equiv × β) × α)

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 γ] :
measurable_equiv ((α × β) × γ) × β × γ)

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 δ] :
measurable_equiv α βmeasurable_equiv γ δmeasurable_equiv γ) δ)

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

A set is equivalent to its image under a function f as measurable spaces, if f is an injective measurable function that sends measurable sets to measurable sets.

Equations
def measurable_equiv.set.range {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (f : α → β) :
function.injective fmeasurable f(∀ (s : set α), is_measurable sis_measurable (f '' s))measurable_equiv α (set.range f)

The domain of f is equivalent to its range as measurable spaces, if f is an injective measurable function that sends measurable sets to measurable sets.

Equations

α is equivalent to its image in α ⊕ β as measurable spaces.

Equations

β 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 γ] :
measurable_equiv ((α β) × γ) × γ β × γ)

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 γ] :
measurable_equiv × γ)) × β α × γ)

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 δ] :
measurable_equiv ((α β) × δ)) ((α × γ α × δ) β × γ β × δ)

Products distribute over sums as measurable spaces.

Equations
def is_pi_system {α : Type u_1} :
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_7Type 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 α} :
pairwise (disjoint on f)(∀ (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 α} :
d.has s₁d.has s₂s₁ s₂ d.has (s₁ s₂)

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

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 α)} :
(∀ (t : set α), t sd.has t)measurable_space.dynkin_system.generate s d

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

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