Measurable spaces and measurable functions

This file provides properties of measurable spaces and the functions and isomorphisms between them. The definition of a measurable space is in Mathlib/MeasureTheory/MeasurableSpace/Defs.lean.

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. A function f : α → β induces a Galois connection between the lattices of σ-algebras on α and β.

Implementation notes

Measurability of a function f : α → β between measurable spaces is defined in terms of the Galois connection induced by f.

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, dynkin system, π-λ theorem, π-system

def MeasurableSpace.map {α : Type u_1} {β : Type u_2} (f : α → β) (m : MeasurableSpace α) : MeasurableSpace β

The forward image of a measurable space under a function. map f m contains the sets s : Set β whose preimage under f is measurable.

Equations

• MeasurableSpace.map f m = { MeasurableSet' := fun (s : Set β) => MeasurableSet (f ⁻¹' s), measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }

theorem MeasurableSpace.map_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : α → β} {s : Set β} : MeasurableSet s ↔ MeasurableSet (f ⁻¹' s)

@[simp]

theorem MeasurableSpace.map_id {α : Type u_1} {m : MeasurableSpace α} : MeasurableSpace.map id m = m

@[simp]

theorem MeasurableSpace.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : α → β} {g : β → γ} : MeasurableSpace.map g (MeasurableSpace.map f m) = MeasurableSpace.map (g ∘ f) m

def MeasurableSpace.comap {α : Type u_1} {β : Type u_2} (f : α → β) (m : MeasurableSpace β) : MeasurableSpace α

The reverse image of a measurable space under a function. comap f m contains the sets s : Set α such that s is the f-preimage of a measurable set in β.

Equations

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

theorem MeasurableSpace.measurableSet_comap {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace β} : MeasurableSet s ↔ ∃ (s' : Set β), MeasurableSet s' ∧ f ⁻¹' s' = s

theorem MeasurableSpace.comap_eq_generateFrom {α : Type u_1} {β : Type u_2} (m : MeasurableSpace β) (f : α → β) : MeasurableSpace.comap f m = generateFrom {t : Set α | ∃ (s : Set β), MeasurableSet s ∧ f ⁻¹' s = t}

@[simp]

theorem MeasurableSpace.comap_id {α : Type u_1} {m : MeasurableSpace α} : MeasurableSpace.comap id m = m

@[simp]

theorem MeasurableSpace.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : β → α} {g : γ → β} : MeasurableSpace.comap g (MeasurableSpace.comap f m) = MeasurableSpace.comap (f ∘ g) m

theorem MeasurableSpace.comap_le_iff_le_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m' : MeasurableSpace β} {f : α → β} : MeasurableSpace.comap f m' ≤ m ↔ m' ≤ MeasurableSpace.map f m

theorem MeasurableSpace.gc_comap_map {α : Type u_1} {β : Type u_2} (f : α → β) : GaloisConnection (MeasurableSpace.comap f) (MeasurableSpace.map f)

theorem MeasurableSpace.map_mono {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {f : α → β} (h : m₁ ≤ m₂) : MeasurableSpace.map f m₁ ≤ MeasurableSpace.map f m₂

theorem MeasurableSpace.monotone_map {α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (MeasurableSpace.map f)

theorem MeasurableSpace.comap_mono {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {g : β → α} (h : m₁ ≤ m₂) : MeasurableSpace.comap g m₁ ≤ MeasurableSpace.comap g m₂

theorem MeasurableSpace.monotone_comap {α : Type u_1} {β : Type u_2} {g : β → α} : Monotone (MeasurableSpace.comap g)

@[simp]

theorem MeasurableSpace.comap_bot {α : Type u_1} {β : Type u_2} {g : β → α} : MeasurableSpace.comap g ⊥ = ⊥

@[simp]

theorem MeasurableSpace.comap_sup {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {g : β → α} : MeasurableSpace.comap g (m₁ ⊔ m₂) = MeasurableSpace.comap g m₁ ⊔ MeasurableSpace.comap g m₂

@[simp]

theorem MeasurableSpace.comap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort uι} {g : β → α} {m : ι → MeasurableSpace α} : MeasurableSpace.comap g (⨆ (i : ι), m i) = ⨆ (i : ι), MeasurableSpace.comap g (m i)

@[simp]

theorem MeasurableSpace.map_top {α : Type u_1} {β : Type u_2} {f : α → β} : MeasurableSpace.map f ⊤ = ⊤

@[simp]

theorem MeasurableSpace.map_inf {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {f : α → β} : MeasurableSpace.map f (m₁ ⊓ m₂) = MeasurableSpace.map f m₁ ⊓ MeasurableSpace.map f m₂

@[simp]

theorem MeasurableSpace.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort uι} {f : α → β} {m : ι → MeasurableSpace α} : MeasurableSpace.map f (⨅ (i : ι), m i) = ⨅ (i : ι), MeasurableSpace.map f (m i)

theorem MeasurableSpace.comap_map_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : α → β} : MeasurableSpace.comap f (MeasurableSpace.map f m) ≤ m

theorem MeasurableSpace.le_map_comap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : β → α} : m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m)

@[simp]

theorem MeasurableSpace.map_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} (b : β) : MeasurableSpace.map (fun (_a : α) => b) m = ⊤

@[simp]

theorem MeasurableSpace.comap_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (b : β) : MeasurableSpace.comap (fun (_a : α) => b) m = ⊥

theorem MeasurableSpace.comap_generateFrom {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)} : MeasurableSpace.comap f (generateFrom s) = generateFrom (Set.preimage f '' s)

theorem measurable_iff_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} : Measurable f ↔ m₂ ≤ MeasurableSpace.map f m₁

theorem Measurable.of_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} : m₂ ≤ MeasurableSpace.map f m₁ → Measurable f

Alias of the reverse direction of measurable_iff_le_map.

theorem Measurable.le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} : Measurable f → m₂ ≤ MeasurableSpace.map f m₁

Alias of the forward direction of measurable_iff_le_map.

theorem measurable_iff_comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} : Measurable f ↔ MeasurableSpace.comap f m₂ ≤ m₁

theorem Measurable.comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} : Measurable f → MeasurableSpace.comap f m₂ ≤ m₁

Alias of the forward direction of measurable_iff_comap_le.

theorem Measurable.of_comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} : MeasurableSpace.comap f m₂ ≤ m₁ → Measurable f

Alias of the reverse direction of measurable_iff_comap_le.

theorem comap_measurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (f : α → β) : Measurable f

theorem Measurable.mono {α : Type u_1} {β : Type u_2} {ma ma' : MeasurableSpace α} {mb mb' : MeasurableSpace β} {f : α → β} (hf : Measurable f) (ha : ma ≤ ma') (hb : mb' ≤ mb) : Measurable f

theorem Measurable.iSup' {α : Type u_1} {β : Type u_2} {ι : Sort uι} {mα : ι → MeasurableSpace α} {x✝ : MeasurableSpace β} {f : α → β} (i₀ : ι) (h : Measurable f) : Measurable f

theorem Measurable.sup_of_left {α : Type u_1} {β : Type u_2} {mα mα' : MeasurableSpace α} {x✝ : MeasurableSpace β} {f : α → β} (h : Measurable f) : Measurable f

theorem Measurable.sup_of_right {α : Type u_1} {β : Type u_2} {mα mα' : MeasurableSpace α} {x✝ : MeasurableSpace β} {f : α → β} (h : Measurable f) : Measurable f

theorem measurable_id'' {α : Type u_1} {m mα : MeasurableSpace α} (hm : m ≤ mα) : Measurable id

theorem measurable_from_top {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {f : α → β} : Measurable f

theorem measurable_generateFrom {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set (Set β)} {f : α → β} (h : ∀ t ∈ s, MeasurableSet (f ⁻¹' t)) : Measurable f

theorem Subsingleton.measurable {α : Type u_1} {β : Type u_2} {f : α → β} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton α] : Measurable f

theorem measurable_of_subsingleton_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton β] (f : α → β) : Measurable f

theorem measurable_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [One α] : Measurable 1

theorem measurable_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Zero α] : Measurable 0

theorem measurable_of_empty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty α] (f : α → β) : Measurable f

theorem measurable_of_empty_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty β] (f : α → β) : Measurable f

theorem measurable_const' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : ∀ (x y : β), f x = f y) : Measurable f

A version of measurable_const that assumes f x = f y for all x, y. This version works for functions between empty types.

theorem measurable_natCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [NatCast α] (n : ℕ) : Measurable ↑n

theorem measurable_intCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IntCast α] (n : ℤ) : Measurable ↑n

theorem measurable_of_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (f : α → β) : Measurable f

theorem measurable_of_finite {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Finite α] [MeasurableSingletonClass α] (f : α → β) : Measurable f

theorem Measurable.iterate {α : Type u_1} {m : MeasurableSpace α} {f : α → α} (hf : Measurable f) (n : ℕ) : Measurable f^[n]

theorem measurableSet_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (hf : Measurable f) (ht : MeasurableSet t) : MeasurableSet (f ⁻¹' t)

theorem MeasurableSet.preimage {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (ht : MeasurableSet t) (hf : Measurable f) : MeasurableSet (f ⁻¹' t)

theorem Measurable.piecewise {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x✝ : DecidablePred fun (x : α) => x ∈ s} (hs : MeasurableSet s) (hf : Measurable f) (hg : Measurable g) : Measurable (s.piecewise f g)

theorem Measurable.ite {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : α → Prop} {x✝ : DecidablePred p} (hp : MeasurableSet {a : α | p a}) (hf : Measurable f) (hg : Measurable g) : Measurable fun (x : α) => if p x then f x else g x

This is slightly different from Measurable.piecewise. It can be used to show Measurable (ite (x=0) 0 1) by exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const, but replacing Measurable.ite by Measurable.piecewise in that example proof does not work.

theorem Measurable.indicator {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] (hf : Measurable f) (hs : MeasurableSet s) : Measurable (s.indicator f)

theorem measurable_indicator_const_iff {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (b : β) [NeZero b] : Measurable (s.indicator fun (x : α) => b) ↔ MeasurableSet s

The measurability of a set A is equivalent to the measurability of the indicator function which takes a constant value b ≠ 0 on a set A and 0 elsewhere.

theorem measurableSet_mulSupport {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [One β] [MeasurableSingletonClass β] (hf : Measurable f) : MeasurableSet (Function.mulSupport f)

theorem measurableSet_support {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (hf : Measurable f) : MeasurableSet (Function.support f)

theorem Measurable.measurable_of_countable_ne {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] (hf : Measurable f) (h : {x : α | f x ≠ g x}.Countable) : Measurable g

If a function coincides with a measurable function outside of a countable set, it is measurable.

def IsCountablySpanning {α : Type u_1} (C : Set (Set α)) : Prop

We say that a collection of sets is countably spanning if a countable subset spans the whole type. This is a useful condition in various parts of measure theory. For example, it is a needed condition to show that the product of two collections generate the product sigma algebra, see generateFrom_prod_eq.

Equations

• IsCountablySpanning C = ∃ (s : ℕ → Set α), (∀ (n : ℕ), s n ∈ C) ∧ ⋃ (n : ℕ), s n = Set.univ

theorem isCountablySpanning_measurableSet {α : Type u_1} [MeasurableSpace α] : IsCountablySpanning {s : Set α | MeasurableSet s}

theorem IsCountablySpanning.prod {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C) (hD : IsCountablySpanning D) : IsCountablySpanning (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D)

Rectangles of countably spanning sets are countably spanning.