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.

References

• https://en.wikipedia.org/wiki/Measurable_space
• https://en.wikipedia.org/wiki/Sigma-algebra
• https://en.wikipedia.org/wiki/Dynkin_system

Tags

measurable space, σ-algebra, measurable function

class MeasurableSpace (α : Type u_7) : Type u_7

• MeasurableSet' : Set α → Prop

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

• measurableSet_empty : MeasurableSpace.MeasurableSet' s ∅

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

• measurableSet_compl : ∀ (s_1 : Set α), MeasurableSpace.MeasurableSet' s s_1 → MeasurableSpace.MeasurableSet' s s_1ᶜ

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

• measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSpace.MeasurableSet' s (f i)) → MeasurableSpace.MeasurableSet' s (⋃ (i : ℕ), f i)

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

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

instance instMeasurableSpaceOrderDual {α : Type u_1} [h : MeasurableSpace α] : MeasurableSpace αᵒᵈ

Equations

• instMeasurableSpaceOrderDual = h

def MeasurableSet {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop

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

Equations

• MeasurableSet s = MeasurableSpace.MeasurableSet' inst s

def MeasureTheory.«termMeasurableSet[_]» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasurableSet.empty {α : Type u_1} [MeasurableSpace α] : MeasurableSet ∅

theorem MeasurableSet.compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} : MeasurableSet s → MeasurableSet sᶜ

theorem MeasurableSet.of_compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} (h : MeasurableSet sᶜ) : MeasurableSet s

@[simp]

theorem MeasurableSet.compl_iff {α : Type u_1} {s : Set α} {m : MeasurableSpace α} : MeasurableSet sᶜ ↔ MeasurableSet s

@[simp]

theorem MeasurableSet.univ {α : Type u_1} {m : MeasurableSpace α} : MeasurableSet Set.univ

theorem Subsingleton.measurableSet {α : Type u_1} {m : MeasurableSpace α} [Subsingleton α] {s : Set α} : MeasurableSet s

theorem MeasurableSet.congr {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (h : s = t) : MeasurableSet t

theorem MeasurableSet.iUnion {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] ⦃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 : MeasurableSpace α} [Encodable β] ⦃f : β → Set α⦄ (h : ∀ (b : β), MeasurableSet (f b)) (n : ℕ) : MeasurableSet (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)

theorem MeasurableSet.biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : Set.Countable s) (h : ∀ (b : β), b ∈ s → MeasurableSet (f b)) : MeasurableSet (⋃ (b : β) (_ : b ∈ s), f b)

theorem Set.Finite.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : Set.Finite s) (h : ∀ (b : β), b ∈ s → MeasurableSet (f b)) : MeasurableSet (⋃ (b : β) (_ : b ∈ s), f b)

theorem Finset.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} (s : Finset β) (h : ∀ (b : β), b ∈ s → MeasurableSet (f b)) : MeasurableSet (⋃ (b : β) (_ : b ∈ s), f b)

theorem MeasurableSet.sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : Set.Countable s) (h : ∀ (t : Set α), t ∈ s → MeasurableSet t) : MeasurableSet (⋃₀ s)

theorem Set.Finite.measurableSet_sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : Set.Finite s) (h : ∀ (t : Set α), t ∈ s → MeasurableSet t) : MeasurableSet (⋃₀ s)

theorem MeasurableSet.iInter {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] {f : ι → Set α} (h : ∀ (b : ι), MeasurableSet (f b)) : MeasurableSet (⋂ (b : ι), f b)

theorem MeasurableSet.biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : Set.Countable s) (h : ∀ (b : β), b ∈ s → MeasurableSet (f b)) : MeasurableSet (⋂ (b : β) (_ : b ∈ s), f b)

theorem Set.Finite.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : Set.Finite s) (h : ∀ (b : β), b ∈ s → MeasurableSet (f b)) : MeasurableSet (⋂ (b : β) (_ : b ∈ s), f b)

theorem Finset.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} (s : Finset β) (h : ∀ (b : β), b ∈ s → MeasurableSet (f b)) : MeasurableSet (⋂ (b : β) (_ : b ∈ s), f b)

theorem MeasurableSet.sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : Set.Countable s) (h : ∀ (t : Set α), t ∈ s → MeasurableSet t) : MeasurableSet (⋂₀ s)

theorem Set.Finite.measurableSet_sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : Set.Finite s) (h : ∀ (t : Set α), t ∈ s → MeasurableSet t) : MeasurableSet (⋂₀ s)

@[simp]

theorem MeasurableSet.union {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∪ s₂)

@[simp]

theorem MeasurableSet.inter {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∩ s₂)

@[simp]

theorem MeasurableSet.diff {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ \ s₂)

@[simp]

theorem MeasurableSet.symmDiff {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∆ s₂)

@[simp]

theorem MeasurableSet.ite {α : Type u_1} {m : MeasurableSpace α} {t : Set α} {s₁ : Set α} {s₂ : Set α} (ht : MeasurableSet t) (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (Set.ite t s₁ s₂)

theorem MeasurableSet.ite' {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} {p : Prop} (hs : p → MeasurableSet s) (ht : ¬p → MeasurableSet t) : MeasurableSet (if p then s else t)

@[simp]

theorem MeasurableSet.cond {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) {i : Bool} : MeasurableSet (bif i then s₁ else s₂)

@[simp]

theorem MeasurableSet.disjointed {α : Type u_1} {m : MeasurableSpace α} {f : ℕ → Set α} (h : ∀ (i : ℕ), MeasurableSet (f i)) (n : ℕ) : MeasurableSet (disjointed f n)

theorem MeasurableSet.const {α : Type u_1} {m : MeasurableSpace α} (p : Prop) : MeasurableSet {_a | p}

theorem nonempty_measurable_superset {α : Type u_1} {m : MeasurableSpace α} (s : Set α) : Nonempty { t // s ⊆ t ∧ MeasurableSet t }

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

theorem MeasurableSpace.measurableSet_injective {α : Type u_1} : Function.Injective (@MeasurableSet α)

theorem MeasurableSpace.ext {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} (h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s) : m₁ = m₂

theorem MeasurableSpace.ext_iff {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} : m₁ = m₂ ↔ ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s

class MeasurableSingletonClass (α : Type u_7) [MeasurableSpace α] : Prop

• measurableSet_singleton : ∀ (x : α), MeasurableSet {x}

  A singleton is a measurable set.

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

@[simp]

theorem MeasurableSet.singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) : MeasurableSet {a}

theorem measurableSet_eq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} : MeasurableSet {x | x = a}

theorem MeasurableSet.insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : MeasurableSet s) (a : α) : MeasurableSet (insert a s)

@[simp]

theorem measurableSet_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} {s : Set α} : MeasurableSet (insert a s) ↔ MeasurableSet s

theorem Set.Subsingleton.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : Set.Subsingleton s) : MeasurableSet s

theorem Set.Finite.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : Set.Finite s) : MeasurableSet s

theorem Finset.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α) : MeasurableSet ↑s

theorem Set.Countable.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : Set.Countable s) : MeasurableSet s

def MeasurableSpace.copy {α : Type u_1} (m : MeasurableSpace α) (p : Set α → Prop) (h : ∀ (s : Set α), p s ↔ MeasurableSet s) : MeasurableSpace α

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

Equations

• One or more equations did not get rendered due to their size.

theorem MeasurableSpace.measurableSet_copy {α : Type u_1} {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ (s : Set α), p s ↔ MeasurableSet s) {s : Set α} : MeasurableSet s ↔ p s

theorem MeasurableSpace.copy_eq {α : Type u_1} {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ (s : Set α), p s ↔ MeasurableSet s) : MeasurableSpace.copy m p h = m

instance MeasurableSpace.instLEMeasurableSpace {α : Type u_1} : LE (MeasurableSpace α)

Equations

• MeasurableSpace.instLEMeasurableSpace = { le := fun m₁ m₂ => ∀ (s : Set α), MeasurableSet s → MeasurableSet s }

theorem MeasurableSpace.le_def {α : Type u_7} {a : MeasurableSpace α} {b : MeasurableSpace α} : a ≤ b ↔ a.MeasurableSet' ≤ b.MeasurableSet'

instance MeasurableSpace.instPartialOrderMeasurableSpace {α : Type u_1} : PartialOrder (MeasurableSpace α)

Equations

• One or more equations did not get rendered due to their size.

inductive MeasurableSpace.GenerateMeasurable {α : Type u_1} (s : Set (Set α)) : Set α → Prop

• basic: ∀ {α : Type u_1} {s : Set (Set α)} (u : Set α), u ∈ s → MeasurableSpace.GenerateMeasurable s u
• empty: ∀ {α : Type u_1} {s : Set (Set α)}, MeasurableSpace.GenerateMeasurable s ∅
• compl: ∀ {α : Type u_1} {s : Set (Set α)} (t : Set α), MeasurableSpace.GenerateMeasurable s t → MeasurableSpace.GenerateMeasurable s tᶜ
• iUnion: ∀ {α : Type u_1} {s : Set (Set α)} (f : ℕ → Set α), (∀ (n : ℕ), MeasurableSpace.GenerateMeasurable s (f n)) → MeasurableSpace.GenerateMeasurable s (⋃ (i : ℕ), f i)

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

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

Construct the smallest measure space containing a collection of basic sets

Equations

• One or more equations did not get rendered due to their size.

theorem MeasurableSpace.measurableSet_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) : MeasurableSet t

theorem MeasurableSpace.generateFrom_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 : MeasurableSet s) : p s

theorem MeasurableSpace.generateFrom_le {α : Type u_1} {s : Set (Set α)} {m : MeasurableSpace α} (h : ∀ (t : Set α), t ∈ s → MeasurableSet t) : MeasurableSpace.generateFrom s ≤ m

theorem MeasurableSpace.generateFrom_le_iff {α : Type u_1} {s : Set (Set α)} (m : MeasurableSpace α) : MeasurableSpace.generateFrom s ≤ m ↔ s ⊆ {t | MeasurableSet t}

@[simp]

theorem MeasurableSpace.generateFrom_measurableSet {α : Type u_1} [MeasurableSpace α] : MeasurableSpace.generateFrom {s | MeasurableSet s} = inst✝

theorem MeasurableSpace.forall_generateFrom_mem_iff_mem_iff {α : Type u_1} {S : Set (Set α)} {x : α} {y : α} : (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)

def MeasurableSpace.mkOfClosure {α : Type u_1} (g : Set (Set α)) (hg : {t | MeasurableSet t} = g) : MeasurableSpace α

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

• MeasurableSpace.mkOfClosure g hg = MeasurableSpace.copy (MeasurableSpace.generateFrom g) (fun x => x ∈ g) (_ : ∀ (x : Set α), x ∈ g ↔ x ∈ fun s => MeasurableSpace.GenerateMeasurable g s)

theorem MeasurableSpace.mkOfClosure_sets {α : Type u_1} {s : Set (Set α)} {hs : {t | MeasurableSet t} = s} : MeasurableSpace.mkOfClosure s hs = MeasurableSpace.generateFrom s

def MeasurableSpace.giGenerateFrom {α : Type u_1} : GaloisInsertion MeasurableSpace.generateFrom fun m => {t | MeasurableSet t}

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

• One or more equations did not get rendered due to their size.

instance MeasurableSpace.instCompleteLatticeMeasurableSpace {α : Type u_1} : CompleteLattice (MeasurableSpace α)

Equations

• MeasurableSpace.instCompleteLatticeMeasurableSpace = GaloisInsertion.liftCompleteLattice MeasurableSpace.giGenerateFrom

instance MeasurableSpace.instInhabitedMeasurableSpace {α : Type u_1} : Inhabited (MeasurableSpace α)

Equations

• MeasurableSpace.instInhabitedMeasurableSpace = { default := ⊤ }

theorem MeasurableSpace.generateFrom_mono {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} (h : s ⊆ t) : MeasurableSpace.generateFrom s ≤ MeasurableSpace.generateFrom t

theorem MeasurableSpace.generateFrom_sup_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} : MeasurableSpace.generateFrom s ⊔ MeasurableSpace.generateFrom t = MeasurableSpace.generateFrom (s ∪ t)

theorem MeasurableSpace.generateFrom_singleton_empty {α : Type u_1} : MeasurableSpace.generateFrom {∅} = ⊥

theorem MeasurableSpace.generateFrom_singleton_univ {α : Type u_1} : MeasurableSpace.generateFrom {Set.univ} = ⊥

@[simp]

theorem MeasurableSpace.generateFrom_insert_univ {α : Type u_1} (S : Set (Set α)) : MeasurableSpace.generateFrom (insert Set.univ S) = MeasurableSpace.generateFrom S

@[simp]

theorem MeasurableSpace.generateFrom_insert_empty {α : Type u_1} (S : Set (Set α)) : MeasurableSpace.generateFrom (insert ∅ S) = MeasurableSpace.generateFrom S

theorem MeasurableSpace.measurableSet_bot_iff {α : Type u_1} {s : Set α} : MeasurableSet s ↔ s = ∅ ∨ s = Set.univ

@[simp]

theorem MeasurableSpace.measurableSet_top {α : Type u_1} {s : Set α} : MeasurableSet s

@[simp]

theorem MeasurableSpace.measurableSet_inf {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

@[simp]

theorem MeasurableSpace.measurableSet_sInf {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α} : MeasurableSet s ↔ ∀ (m : MeasurableSpace α), m ∈ ms → MeasurableSet s

theorem MeasurableSpace.measurableSet_iInf {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s

theorem MeasurableSpace.measurableSet_sup {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable (MeasurableSet ∪ MeasurableSet) s

theorem MeasurableSpace.measurableSet_sSup {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α} : MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s | ∃ m, m ∈ ms ∧ MeasurableSet s} s

theorem MeasurableSpace.measurableSet_iSup {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s | ∃ i, MeasurableSet s} s

theorem MeasurableSpace.measurableSpace_iSup_eq {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α) : ⨆ (n : ι), m n = MeasurableSpace.generateFrom {s | ∃ n, MeasurableSet s}

theorem MeasurableSpace.generateFrom_iUnion_measurableSet {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α) : MeasurableSpace.generateFrom (⋃ (n : ι), {t | MeasurableSet t}) = ⨆ (n : ι), m n

def Measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Prop

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

Equations

• Measurable f = ∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (f ⁻¹' t)

def MeasureTheory.«termMeasurable[_]» : Lean.ParserDescr

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.

theorem measurable_id {α : Type u_1} : ∀ {x : MeasurableSpace α}, Measurable id

theorem measurable_id' {α : Type u_1} : ∀ {x : MeasurableSpace α}, Measurable fun a => a

theorem Measurable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable (g ∘ f)

theorem Measurable.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable fun x => g (f x)

@[simp]

theorem measurable_const {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {a : α}, Measurable fun x => a

theorem Measurable.le {β : Type u_2} {α : Type u_7} {m : MeasurableSpace α} {m0 : MeasurableSpace α} : ∀ {x : MeasurableSpace β}, m ≤ m0 → ∀ {f : α → β}, Measurable f → Measurable f

theorem MeasurableSpace.Top.measurable {α : Type u_7} {β : Type u_8} [MeasurableSpace β] (f : α → β) : Measurable f