mathlib3 documentation

measure_theory.measurable_space_def

Measurable spaces and measurable functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
@[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]
@[simp, measurability]
@[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 s measurable_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 s measurable_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 s measurable_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 s measurable_set t) :
theorem set.finite.measurable_set_sUnion {α : Type u_1} {m : measurable_space α} {s : set (set α)} (hs : s.finite) (h : (t : set α), t s measurable_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 s measurable_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 s measurable_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 s measurable_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 s measurable_set t) :
theorem set.finite.measurable_set_sInter {α : Type u_1} {m : measurable_space α} {s : set (set α)} (hs : s.finite) (h : (t : set α), t s measurable_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₂)
theorem measurable_set.ite' {α : Type u_1} {m : measurable_space α} {s t : set α} {p : Prop} (hs : p measurable_set s) (ht : ¬p measurable_set t) :
@[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 : ) :
@[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]
@[protected, measurability]
@[protected, instance]
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 C p t) (h_empty : p ) (h_compl : (t : set α), p t p t) (h_Union : (f : set α), ( (n : ), p (f n)) p ( (i : ), f i)) {s : set α} (hs : measurable_set s) :
p s
@[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]
@[simp]
theorem measurable_space.measurable_set_infi {α : 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}
theorem measurable_space.generate_from_Union_measurable_set {α : Type u_1} {ι : Sort u_6} (m : ι measurable_space α) :
measurable_space.generate_from ( (n : ι), {t : set α | measurable_set t}) = (n : ι), m n
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) :
theorem measurable_space.top.measurable {α : Type u_1} {β : Type u_2} [measurable_space β] (f : α β) :