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

## Tags #

measurable space, σ-algebra, measurable function

class MeasurableSpace (α : Type u_7) :
Type u_7

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

• MeasurableSet' : Set αProp

Predicate saying that a given set is measurable. Use MeasurableSet in the root namespace instead.

• measurableSet_empty : self.MeasurableSet'

The empty set is a measurable set. Use MeasurableSet.empty instead.

• measurableSet_compl : ∀ (s : Set α), self.MeasurableSet' sself.MeasurableSet' s

The complement of a measurable set is a measurable set. Use MeasurableSet.compl instead.

• measurableSet_iUnion : ∀ (f : Set α), (∀ (i : ), self.MeasurableSet' (f i))self.MeasurableSet' (⋃ (i : ), f i)

The union of a sequence of measurable sets is a measurable set. Use a more general MeasurableSet.iUnion instead.

Instances
theorem MeasurableSpace.measurableSet_empty {α : Type u_7} (self : ) :
self.MeasurableSet'

The empty set is a measurable set. Use MeasurableSet.empty instead.

theorem MeasurableSpace.measurableSet_compl {α : Type u_7} (self : ) (s : Set α) :
self.MeasurableSet' sself.MeasurableSet' s

The complement of a measurable set is a measurable set. Use MeasurableSet.compl instead.

theorem MeasurableSpace.measurableSet_iUnion {α : Type u_7} (self : ) (f : Set α) :
(∀ (i : ), self.MeasurableSet' (f i))self.MeasurableSet' (⋃ (i : ), f i)

The union of a sequence of measurable sets is a measurable set. Use a more general MeasurableSet.iUnion instead.

instance instMeasurableSpaceOrderDual {α : Type u_1} [h : ] :
Equations
• instMeasurableSpaceOrderDual = h
def MeasurableSet {α : Type u_1} [] (s : Set α) :

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

Equations
• = inst.MeasurableSet' s
Instances For

Notation for MeasurableSet with respect to a non-standard σ-algebra.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasurableSet.empty {α : Type u_1} [] :
theorem MeasurableSet.compl {α : Type u_1} {s : Set α} {m : } :
theorem MeasurableSet.of_compl {α : Type u_1} {s : Set α} {m : } (h : ) :
@[simp]
theorem MeasurableSet.compl_iff {α : Type u_1} {s : Set α} {m : } :
@[simp]
theorem MeasurableSet.univ {α : Type u_1} {m : } :
MeasurableSet Set.univ
theorem Subsingleton.measurableSet {α : Type u_1} {m : } [] {s : Set α} :
theorem MeasurableSet.congr {α : Type u_1} {m : } {s : Set α} {t : Set α} (hs : ) (h : s = t) :
theorem MeasurableSet.iUnion {α : Type u_1} {ι : Sort u_6} {m : } [] ⦃f : ιSet α (h : ∀ (b : ι), MeasurableSet (f b)) :
MeasurableSet (⋃ (b : ι), f b)
@[deprecated MeasurableSet.iUnion]
theorem MeasurableSet.biUnion_decode₂ {α : Type u_1} {β : Type u_2} {m : } [] ⦃f : βSet α (h : ∀ (b : β), MeasurableSet (f b)) (n : ) :
MeasurableSet (b, f b)
theorem MeasurableSet.biUnion {α : Type u_1} {β : Type u_2} {m : } {f : βSet α} {s : Set β} (hs : s.Countable) (h : bs, MeasurableSet (f b)) :
MeasurableSet (bs, f b)
theorem Set.Finite.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : } {f : βSet α} {s : Set β} (hs : s.Finite) (h : bs, MeasurableSet (f b)) :
MeasurableSet (bs, f b)
theorem Finset.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : } {f : βSet α} (s : ) (h : bs, MeasurableSet (f b)) :
MeasurableSet (bs, f b)
theorem MeasurableSet.sUnion {α : Type u_1} {m : } {s : Set (Set α)} (hs : s.Countable) (h : ts, ) :
theorem Set.Finite.measurableSet_sUnion {α : Type u_1} {m : } {s : Set (Set α)} (hs : s.Finite) (h : ts, ) :
theorem MeasurableSet.iInter {α : Type u_1} {ι : Sort u_6} {m : } [] {f : ιSet α} (h : ∀ (b : ι), MeasurableSet (f b)) :
MeasurableSet (⋂ (b : ι), f b)
theorem MeasurableSet.biInter {α : Type u_1} {β : Type u_2} {m : } {f : βSet α} {s : Set β} (hs : s.Countable) (h : bs, MeasurableSet (f b)) :
MeasurableSet (bs, f b)
theorem Set.Finite.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : } {f : βSet α} {s : Set β} (hs : s.Finite) (h : bs, MeasurableSet (f b)) :
MeasurableSet (bs, f b)
theorem Finset.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : } {f : βSet α} (s : ) (h : bs, MeasurableSet (f b)) :
MeasurableSet (bs, f b)
theorem MeasurableSet.sInter {α : Type u_1} {m : } {s : Set (Set α)} (hs : s.Countable) (h : ts, ) :
theorem Set.Finite.measurableSet_sInter {α : Type u_1} {m : } {s : Set (Set α)} (hs : s.Finite) (h : ts, ) :
@[simp]
theorem MeasurableSet.union {α : Type u_1} {m : } {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) :
MeasurableSet (s₁ s₂)
@[simp]
theorem MeasurableSet.inter {α : Type u_1} {m : } {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) :
MeasurableSet (s₁ s₂)
@[simp]
theorem MeasurableSet.diff {α : Type u_1} {m : } {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) :
MeasurableSet (s₁ \ s₂)
@[simp]
theorem MeasurableSet.himp {α : Type u_1} {m : } {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) :
MeasurableSet (s₁ s₂)
@[simp]
theorem MeasurableSet.symmDiff {α : Type u_1} {m : } {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) :
@[simp]
theorem MeasurableSet.bihimp {α : Type u_1} {m : } {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) :
MeasurableSet (bihimp s₁ s₂)
@[simp]
theorem MeasurableSet.ite {α : Type u_1} {m : } {t : Set α} {s₁ : Set α} {s₂ : Set α} (ht : ) (h₁ : ) (h₂ : ) :
MeasurableSet (t.ite s₁ s₂)
theorem MeasurableSet.ite' {α : Type u_1} {m : } {s : Set α} {t : Set α} {p : Prop} (hs : p) (ht : ¬p) :
MeasurableSet (if p then s else t)
@[simp]
theorem MeasurableSet.cond {α : Type u_1} {m : } {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) {i : Bool} :
MeasurableSet (bif i then s₁ else s₂)
@[simp]
theorem MeasurableSet.disjointed {α : Type u_1} {m : } {f : Set α} (h : ∀ (i : ), MeasurableSet (f i)) (n : ) :
theorem MeasurableSet.const {α : Type u_1} {m : } (p : Prop) :
MeasurableSet {_a : α | p}
theorem nonempty_measurable_superset {α : Type u_1} {m : } (s : Set α) :
Nonempty { t : Set α // s t }

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

theorem MeasurableSpace.ext {α : Type u_1} {m₁ : } {m₂ : } (h : ∀ (s : Set α), ) :
m₁ = m₂
theorem MeasurableSpace.ext_iff {α : Type u_1} {m₁ : } {m₂ : } :
m₁ = m₂ ∀ (s : Set α),
class MeasurableSingletonClass (α : Type u_7) [] :

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

• measurableSet_singleton : ∀ (x : α),

A singleton is a measurable set.

Instances
theorem MeasurableSingletonClass.measurableSet_singleton {α : Type u_7} [] [self : ] (x : α) :

A singleton is a measurable set.

@[simp]
theorem MeasurableSet.singleton {α : Type u_1} [] (a : α) :
theorem measurableSet_eq {α : Type u_1} [] {a : α} :
MeasurableSet {x : α | x = a}
theorem MeasurableSet.insert {α : Type u_1} [] {s : Set α} (hs : ) (a : α) :
@[simp]
theorem measurableSet_insert {α : Type u_1} [] {a : α} {s : Set α} :
theorem Set.Subsingleton.measurableSet {α : Type u_1} [] {s : Set α} (hs : s.Subsingleton) :
theorem Set.Finite.measurableSet {α : Type u_1} [] {s : Set α} (hs : s.Finite) :
theorem Finset.measurableSet {α : Type u_1} [] (s : ) :
theorem Set.Countable.measurableSet {α : Type u_1} [] {s : Set α} (hs : s.Countable) :
def MeasurableSpace.copy {α : Type u_1} (m : ) (p : Set αProp) (h : ∀ (s : Set α), p s ) :

Copy of a MeasurableSpace with a new MeasurableSet equal to the old one. Useful to fix definitional equalities.

Equations
• m.copy p h = { MeasurableSet' := p, measurableSet_empty := , measurableSet_compl := , measurableSet_iUnion := }
Instances For
theorem MeasurableSpace.measurableSet_copy {α : Type u_1} {m : } {p : Set αProp} (h : ∀ (s : Set α), p s ) {s : Set α} :
p s
theorem MeasurableSpace.copy_eq {α : Type u_1} {m : } {p : Set αProp} (h : ∀ (s : Set α), p s ) :
m.copy p h = m
instance MeasurableSpace.instLE {α : Type u_1} :
Equations
• MeasurableSpace.instLE = { le := fun (m₁ m₂ : ) => ∀ (s : Set α), }
theorem MeasurableSpace.le_def {α : Type u_7} {a : } {b : } :
a b a.MeasurableSet' b.MeasurableSet'
Equations
• MeasurableSpace.instPartialOrder = let __src := ;
inductive MeasurableSpace.GenerateMeasurable {α : Type u_1} (s : Set (Set α)) :
Set αProp

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

Instances For
def MeasurableSpace.generateFrom {α : Type u_1} (s : Set (Set α)) :

Construct the smallest measure space containing a collection of basic sets

Equations
• = { MeasurableSet' := , measurableSet_empty := , measurableSet_compl := , measurableSet_iUnion := }
Instances For
theorem MeasurableSpace.measurableSet_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t s) :
theorem MeasurableSpace.generateFrom_induction {α : Type u_1} (p : Set αProp) (C : Set (Set α)) (hC : tC, p 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 : ) :
p s
theorem MeasurableSpace.generateFrom_le {α : Type u_1} {s : Set (Set α)} {m : } (h : ts, ) :
theorem MeasurableSpace.generateFrom_le_iff {α : Type u_1} {s : Set (Set α)} (m : ) :
s {t : Set α | }
theorem MeasurableSpace.forall_generateFrom_mem_iff_mem_iff {α : Type u_1} {S : Set (Set α)} {x : α} {y : α} :
(∀ (s : Set α), (x s y s)) sS, x s y s
def MeasurableSpace.mkOfClosure {α : Type u_1} (g : Set (Set α)) (hg : {t : Set α | } = 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
• = .copy (fun (x : Set α) => x g)
Instances For
theorem MeasurableSpace.mkOfClosure_sets {α : Type u_1} {s : Set (Set α)} {hs : {t : Set α | } = s} :
def MeasurableSpace.giGenerateFrom {α : Type u_1} :
GaloisInsertion MeasurableSpace.generateFrom fun (m : ) => {t : Set α | }

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
• MeasurableSpace.giGenerateFrom = { choice := fun (g : Set (Set α)) (hg : {t : Set α | } g) => , gc := , le_l_u := , choice_eq := }
Instances For
Equations
• MeasurableSpace.instCompleteLattice = MeasurableSpace.giGenerateFrom.liftCompleteLattice
instance MeasurableSpace.instInhabited {α : Type u_1} :
Equations
• MeasurableSpace.instInhabited = { default := }
theorem MeasurableSpace.generateFrom_mono {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} (h : s t) :
theorem MeasurableSpace.generateFrom_sup_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} :
theorem MeasurableSpace.iSup_generateFrom {α : Type u_1} {ι : Sort u_6} (s : ιSet (Set α)) :
⨆ (i : ι), = MeasurableSpace.generateFrom (⋃ (i : ι), s i)
@[simp]
@[simp]
theorem MeasurableSpace.generateFrom_insert_empty {α : Type u_1} (S : Set (Set α)) :
theorem MeasurableSpace.measurableSet_bot_iff {α : Type u_1} {s : Set α} :
s = s = Set.univ
@[simp]
theorem MeasurableSpace.measurableSet_top {α : Type u_1} {s : Set α} :
@[simp]
theorem MeasurableSpace.measurableSet_inf {α : Type u_1} {m₁ : } {m₂ : } {s : Set α} :
@[simp]
theorem MeasurableSpace.measurableSet_sInf {α : Type u_1} {ms : } {s : Set α} :
mms,
theorem MeasurableSpace.measurableSet_iInf {α : Type u_1} {ι : Sort u_7} {m : ι} {s : Set α} :
∀ (i : ι),
theorem MeasurableSpace.measurableSet_sup {α : Type u_1} {m₁ : } {m₂ : } {s : Set α} :
MeasurableSpace.GenerateMeasurable (MeasurableSet MeasurableSet) s
theorem MeasurableSpace.measurableSet_sSup {α : Type u_1} {ms : } {s : Set α} :
MeasurableSpace.GenerateMeasurable {s : Set α | mms, } s
theorem MeasurableSpace.measurableSet_iSup {α : Type u_1} {ι : Sort u_7} {m : ι} {s : Set α} :
MeasurableSpace.GenerateMeasurable {s : Set α | ∃ (i : ι), } s
theorem MeasurableSpace.measurableSpace_iSup_eq {α : Type u_1} {ι : Sort u_6} (m : ι) :
⨆ (n : ι), m n = MeasurableSpace.generateFrom {s : Set α | ∃ (n : ι), }
theorem MeasurableSpace.generateFrom_iUnion_measurableSet {α : Type u_1} {ι : Sort u_6} (m : ι) :
MeasurableSpace.generateFrom (⋃ (n : ι), {t : Set α | }) = ⨆ (n : ι), m n
def Measurable {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :

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

Equations
Instances For

Notation for Measurable with respect to a non-standanrd σ-algebra in the domain.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem measurable_id {α : Type u_1} :
∀ {x : },
theorem measurable_id' {α : Type u_1} :
∀ {x : }, Measurable fun (a : α) => a
theorem Measurable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
∀ {x : } {x_1 : } {x_2 : } {g : βγ} {f : αβ}, Measurable (g f)
theorem Measurable.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
∀ {x : } {x_1 : } {x_2 : } {g : βγ} {f : αβ}, Measurable fun (x : α) => g (f x)
@[simp]
theorem measurable_const {α : Type u_1} {β : Type u_2} :
∀ {x : } {x_1 : } {a : α}, Measurable fun (x : β) => a
theorem Measurable.le {β : Type u_2} {α : Type u_7} {m : } {m0 : } :
∀ {x : }, m m0∀ {f : αβ},
class DiscreteMeasurableSpace (α : Type u_7) [] :

A typeclass mixin for MeasurableSpaces such that all sets are measurable.

Instances
theorem DiscreteMeasurableSpace.forall_measurableSet {α : Type u_7} [] [self : ] (s : Set α) :

Do not use this. Use measurableSet_discrete instead.

instance instDiscreteMeasurableSpace {α : Type u_1} :
Equations
• =
@[instance 100]
Equations
• =
theorem measurableSet_discrete {α : Type u_1} [] (s : Set α) :
theorem measurable_discrete {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :
@[instance 100]

Warning: Creates a typeclass loop with MeasurableSingletonClass.toDiscreteMeasurableSpace. To be monitored.

Equations
• =