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

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

A measurable space is a space equipped with a σ-algebra.

Instances of this typeclass
Instances of other typeclasses for measurable_space
@[protected, 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, measurability]
theorem measurable_set.empty {α : Type u_1} [measurable_space α] :
@[measurability]
theorem measurable_set.compl {α : Type u_1} {s : set α} {m : measurable_space α} :
theorem measurable_set.of_compl {α : Type u_1} {s : set α} {m : measurable_space α} (h : measurable_set s) :
@[simp]
theorem measurable_set.compl_iff {α : Type u_1} {s : set α} {m : measurable_space α} :
@[simp, measurability]
theorem measurable_set.univ {α : Type u_1} {m : measurable_space α} :
@[measurability]
theorem subsingleton.measurable_set {α : Type u_1} {m : measurable_space α} [subsingleton α] {s : set α} :
theorem measurable_set.congr {α : Type u_1} {m : measurable_space α} {s t : set α} (hs : measurable_set s) (h : s = t) :
theorem measurable_set.bUnion_decode₂ {α : Type u_1} {β : Type u_2} {m : measurable_space α} [encodable β] ⦃f : β → set α (h : ∀ (b : β), measurable_set (f b)) (n : ) :
measurable_set (⋃ (b : β) (H : b encodable.decode₂ β n), f b)
@[measurability]
theorem measurable_set.Union {α : Type u_1} {ι : Sort u_6} {m : measurable_space α} [countable ι] ⦃f : ι → set α (h : ∀ (b : ι), measurable_set (f b)) :
measurable_set (⋃ (b : ι), f b)
theorem measurable_set.bUnion {α : Type u_1} {β : Type u_2} {m : 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} {m : 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} {m : 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} {m : measurable_space α} {s : set (set α)} (hs : s.countable) (h : ∀ (t : set α), t smeasurable_set t) :
theorem set.finite.measurable_set_sUnion {α : Type u_1} {m : measurable_space α} {s : set (set α)} (hs : s.finite) (h : ∀ (t : set α), t smeasurable_set t) :
@[measurability]
theorem measurable_set.Inter {α : Type u_1} {ι : Sort u_6} {m : measurable_space α} [countable ι] {f : ι → set α} (h : ∀ (b : ι), measurable_set (f b)) :
measurable_set (⋂ (b : ι), f b)
theorem measurable_set.bInter {α : Type u_1} {β : Type u_2} {m : 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} {m : 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} {m : 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} {m : measurable_space α} {s : set (set α)} (hs : s.countable) (h : ∀ (t : set α), t smeasurable_set t) :
theorem set.finite.measurable_set_sInter {α : Type u_1} {m : measurable_space α} {s : set (set α)} (hs : s.finite) (h : ∀ (t : set α), t smeasurable_set t) :
@[simp, measurability]
theorem measurable_set.union {α : Type u_1} {m : measurable_space α} {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ s₂)
@[simp, measurability]
theorem measurable_set.inter {α : Type u_1} {m : measurable_space α} {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ s₂)
@[simp, measurability]
theorem measurable_set.diff {α : Type u_1} {m : measurable_space α} {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ \ s₂)
@[simp, measurability]
theorem measurable_set.symm_diff {α : Type u_1} {m : measurable_space α} {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
measurable_set (s₁ s₂)
@[simp, measurability]
theorem measurable_set.ite {α : Type u_1} {m : 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, measurability]
theorem measurable_set.cond {α : Type u_1} {m : measurable_space α} {s₁ s₂ : set α} (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) {i : bool} :
measurable_set (cond i s₁ s₂)
@[simp, measurability]
theorem measurable_set.disjointed {α : Type u_1} {m : measurable_space α} {f : set α} (h : ∀ (i : ), measurable_set (f i)) (n : ) :
@[simp, measurability]
theorem measurable_set.const {α : Type u_1} {m : measurable_space α} (p : Prop) :
measurable_set {a : α | p}
theorem nonempty_measurable_superset {α : Type u_1} {m : 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 α), measurable_set s measurable_set s)m₁ = m₂
@[ext]
theorem measurable_space.ext_iff {α : Type u_1} {m₁ m₂ : measurable_space α} :
m₁ = m₂ ∀ (s : set α), measurable_set s measurable_set s
@[measurability]
theorem measurable_set_eq {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {a : α} :
measurable_set {x : α | x = a}
@[measurability]
theorem measurable_set.insert {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {s : set α} (hs : measurable_set s) (a : α) :
@[simp]
theorem set.finite.measurable_set {α : Type u_1} [measurable_space α] [measurable_singleton_class α] {s : set α} (hs : s.finite) :
@[protected, measurability]
@[protected, instance]
def measurable_space.has_le {α : Type u_1} :
Equations
@[protected, 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_induction {α : Type u_1} (p : set α → Prop) (C : set (set α)) (hC : ∀ (t : set α), t Cp t) (h_empty : p ) (h_compl : ∀ (t : set α), p tp t) (h_Union : ∀ (f : set α), (∀ (n : ), p (f n))p (⋃ (i : ), f i)) {s : set α} (hs : measurable_set s) :
p s
theorem measurable_space.generate_from_le {α : Type u_1} {s : set (set α)} {m : measurable_space α} (h : ∀ (t : set α), t smeasurable_set t) :
@[protected]
def measurable_space.mk_of_closure {α : Type u_1} (g : set (set α)) (hg : {t : set α | 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
@[protected, instance]
Equations
@[simp, measurability]
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 α} :
theorem measurable_space.measurable_space_supr_eq {α : Type u_1} {ι : Sort u_6} (m : ι → measurable_space α) :
(⨆ (n : ι), m n) = measurable_space.generate_from {s : set α | ∃ (n : ι), measurable_set s}
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
Instances for measurable
@[measurability]
theorem measurable_id {α : Type u_1} {ma : measurable_space α} :
@[measurability]
theorem measurable_id' {α : Type u_1} {ma : measurable_space α} :
measurable (λ (a : α), a)
theorem measurable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) :
@[simp, measurability]
theorem measurable_const {α : Type u_1} {β : Type u_2} {ma : measurable_space α} {mb : measurable_space β} {a : α} :
measurable (λ (b : β), a)
theorem measurable.le {β : Type u_2} {α : Type u_1} {m m0 : measurable_space α} {mb : measurable_space β} (hm : m m0) {f : α → β} (hf : measurable f) :