mathlib documentation

measure_theory.measurable_space_def

Measurable spaces and measurable functions #

This file defines measurable spaces and measurable functions.

A measurable space is a set equipped with a σ-algebra, a collection of subsets closed under complementation and countable union. A function between measurable spaces is measurable if the preimage of each measurable subset is measurable.

σ-algebras on a fixed set α form a complete lattice. Here we order σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any collection of subsets of α generates a smallest σ-algebra which contains all of them.

Do not add measurability lemmas (which could be tagged with @[measurability]) to this file, since the measurability tactic is downstream from here. Use measure_theory.measurable_space instead.

References #

Tags #

measurable space, σ-algebra, measurable function

@[instance]
Equations
def measurable_set {α : Type u_1} [measurable_space α] :
set α → Prop

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

Equations
@[simp]
theorem measurable_set.empty {α : Type u_1} [measurable_space α] :
theorem measurable_set.compl {α : Type u_1} {s : set α} [measurable_space α] :
theorem measurable_set.of_compl {α : Type u_1} {s : set α} [measurable_space α] (h : measurable_set s) :
@[simp]
theorem measurable_set.compl_iff {α : Type u_1} {s : set α} [measurable_space α] :
@[simp]
theorem subsingleton.measurable_set {α : Type u_1} [measurable_space α] [subsingleton α] {s : set α} :
theorem measurable_set.congr {α : Type u_1} [measurable_space α] {s t : set α} (hs : measurable_set s) (h : s = t) :
theorem measurable_set.bUnion_decode₂ {α : Type u_1} {β : Type u_2} [measurable_space α] [encodable β] ⦃f : β → set α (h : ∀ (b : β), measurable_set (f b)) (n : ) :
measurable_set (⋃ (b : β) (H : b encodable.decode₂ β n), f b)
theorem measurable_set.Union {α : Type u_1} {β : Type u_2} [measurable_space α] [encodable β] ⦃f : β → set α (h : ∀ (b : β), measurable_set (f b)) :
measurable_set (⋃ (b : β), f b)
theorem measurable_set.bUnion {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.countable) (h : ∀ (b : β), b smeasurable_set (f b)) :
measurable_set (⋃ (b : β) (H : b s), f b)
theorem set.finite.measurable_set_bUnion {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.finite) (h : ∀ (b : β), b smeasurable_set (f b)) :
measurable_set (⋃ (b : β) (H : b s), f b)
theorem finset.measurable_set_bUnion {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} (s : finset β) (h : ∀ (b : β), b smeasurable_set (f b)) :
measurable_set (⋃ (b : β) (H : b s), f b)
theorem measurable_set.sUnion {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.countable) (h : ∀ (t : set α), t smeasurable_set t) :
theorem set.finite.measurable_set_sUnion {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.finite) (h : ∀ (t : set α), t smeasurable_set t) :
theorem measurable_set.Union_Prop {α : Type u_1} [measurable_space α] {p : Prop} {f : p → set α} (hf : ∀ (b : p), measurable_set (f b)) :
measurable_set (⋃ (b : p), f b)
theorem measurable_set.Inter {α : Type u_1} {β : Type u_2} [measurable_space α] [encodable β] {f : β → set α} (h : ∀ (b : β), measurable_set (f b)) :
measurable_set (⋂ (b : β), f b)
theorem measurable_set.Union_fintype {α : Type u_1} {β : Type u_2} [measurable_space α] [fintype β] {f : β → set α} (h : ∀ (b : β), measurable_set (f b)) :
measurable_set (⋃ (b : β), f b)
theorem measurable_set.Inter_fintype {α : Type u_1} {β : Type u_2} [measurable_space α] [fintype β] {f : β → set α} (h : ∀ (b : β), measurable_set (f b)) :
measurable_set (⋂ (b : β), f b)
theorem measurable_set.bInter {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.countable) (h : ∀ (b : β), b smeasurable_set (f b)) :
measurable_set (⋂ (b : β) (H : b s), f b)
theorem set.finite.measurable_set_bInter {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} {s : set β} (hs : s.finite) (h : ∀ (b : β), b smeasurable_set (f b)) :
measurable_set (⋂ (b : β) (H : b s), f b)
theorem finset.measurable_set_bInter {α : Type u_1} {β : Type u_2} [measurable_space α] {f : β → set α} (s : finset β) (h : ∀ (b : β), b smeasurable_set (f b)) :
measurable_set (⋂ (b : β) (H : b s), f b)
theorem measurable_set.sInter {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.countable) (h : ∀ (t : set α), t smeasurable_set t) :
theorem set.finite.measurable_set_sInter {α : Type u_1} [measurable_space α] {s : set (set α)} (hs : s.finite) (h : ∀ (t : set α), t smeasurable_set t) :
theorem measurable_set.Inter_Prop {α : Type u_1} [measurable_space α] {p : Prop} {f : p → set α} (hf : ∀ (b : p), measurable_set (f b)) :
measurable_set (⋂ (b : p), f b)
@[simp]
theorem measurable_set.union {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ s₂)
@[simp]
theorem measurable_set.inter {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ s₂)
@[simp]
theorem measurable_set.diff {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ \ s₂)
@[simp]
theorem measurable_set.symm_diff {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ Δ s₂)
@[simp]
theorem measurable_set.ite {α : Type u_1} [measurable_space α] {t s₁ s₂ : set α} (ht : measurable_set t) (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (t.ite s₁ s₂)
@[simp]
theorem measurable_set.cond {α : Type u_1} [measurable_space α] {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) {i : bool} :
measurable_set (cond i s₁ s₂)
@[simp]
theorem measurable_set.disjointed {α : Type u_1} [measurable_space α] {f : set α} (h : ∀ (i : ), measurable_set (f i)) (n : ) :
@[simp]
theorem measurable_set.const {α : Type u_1} [measurable_space α] (p : Prop) :
measurable_set {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₁.measurable_set' s m₂.measurable_set' s)m₁ = m₂
@[ext]
theorem measurable_space.ext_iff {α : Type u_1} {m₁ m₂ : measurable_space α} :
m₁ = m₂ ∀ (s : set α), m₁.measurable_set' s m₂.measurable_set' 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 measurable_set_eq {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {a : α} :
measurable_set {x : α | x = a}
theorem measurable_set.insert {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {s : set α} (hs : measurable_set s) (a : α) :
@[simp]
theorem measurable_set_insert {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {a : α} {s : set α} :
theorem set.finite.measurable_set {α : 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.measurable_set_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.measurable_set' t) :
def measurable_space.mk_of_closure {α : Type u_1} (g : set (set α)) (hg : {t : set α | (measurable_space.generate_from g).measurable_set' t} = g) :

If g is a collection of subsets of α such that the σ-algebra generated from g contains the same sets as g, then g was already a σ-algebra.

Equations

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
@[simp]
theorem measurable_space.measurable_set_top {α : Type u_1} {s : set α} :
@[simp]
theorem measurable_space.measurable_set_inf {α : Type u_1} {m₁ m₂ : measurable_space α} {s : set α} :
@[simp]
theorem measurable_space.measurable_set_Inf {α : Type u_1} {ms : set (measurable_space α)} {s : set α} :
@[simp]
theorem measurable_space.measurable_set_infi {α : Type u_1} {ι : Sort u_2} {m : ι → measurable_space α} {s : set α} :
theorem measurable_space.measurable_set_Sup {α : Type u_1} {ms : set (measurable_space α)} {s : set α} :
theorem measurable_space.measurable_set_supr {α : Type u_1} {ι : Sort u_2} {m : ι → measurable_space α} {s : set α} :
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_id {α : Type u_1} [measurable_space α] :
theorem measurable_id' {α : Type u_1} [measurable_space α] :
measurable (λ (a : α), a)
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) :
@[simp]
theorem measurable_const {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {a : α} :
measurable (λ (b : β), a)