# Constructions for measurable spaces and functions #

This file provides several ways to construct new measurable spaces and functions from old ones: `Quotient`, `Subtype`, `Prod`, `Pi`, etc.

source
theorem measurable_to_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : β → α} (h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})) :
Measurable f
source
theorem measurable_to_countable' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : β → α} (h : ∀ (x : α), MeasurableSet (f ⁻¹' {x})) :
Measurable f
source
theorem ENat.measurable_iff {α : Type u_6} [MeasurableSpace α] {f : α → ℕ∞} :
Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
source
theorem measurable_unit {α : Type u_1} [MeasurableSpace α] (f : Unit → α) :
Measurable f
source
instance ULift.instMeasurableSpace {α : Type u_1} [MeasurableSpace α] :
MeasurableSpace (ULift.{u_6, u_1} α)
Equations

- ULift.instMeasurableSpace = MeasurableSpace.map ULift.up inst✝

source
theorem measurable_down {α : Type u_1} [MeasurableSpace α] :
Measurable ULift.down
source
theorem measurable_up {α : Type u_1} [MeasurableSpace α] :
Measurable ULift.up
source
@[simp]
theorem measurableSet_preimage_down {α : Type u_1} [MeasurableSpace α] {s : Set α} :
MeasurableSet (ULift.down ⁻¹' s) ↔ MeasurableSet s
source
@[simp]
theorem measurableSet_preimage_up {α : Type u_1} [MeasurableSpace α] {s : Set (ULift.{u_6, u_1} α)} :
MeasurableSet (ULift.up ⁻¹' s) ↔ MeasurableSet s
source
theorem measurable_from_nat {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → α} :
Measurable f
source
theorem measurable_to_nat {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℕ} :
(∀ (y : α), MeasurableSet (f ⁻¹' {f y})) → Measurable f
source
theorem measurable_to_bool {α : Type u_1} {mα : MeasurableSpace α} {f : α → Bool} (h : MeasurableSet (f ⁻¹' {true})) :
Measurable f
source
theorem measurable_to_prop {α : Type u_1} {mα : MeasurableSpace α} {f : α → Prop} (h : MeasurableSet (f ⁻¹' {True})) :
Measurable f
source
theorem measurable_findGreatest' {α : Type u_1} {mα : MeasurableSpace α} {p : α → ℕ → Prop} [(x : α) → DecidablePred (p x)] {N : ℕ} (hN : ∀ k ≤ N, MeasurableSet {x : α | Nat.findGreatest (p x) N = k}) :
Measurable fun (x : α) => Nat.findGreatest (p x) N
source
theorem measurable_findGreatest {α : Type u_1} {mα : MeasurableSpace α} {p : α → ℕ → Prop} [(x : α) → DecidablePred (p x)] {N : ℕ} (hN : ∀ k ≤ N, MeasurableSet {x : α | p x k}) :
Measurable fun (x : α) => Nat.findGreatest (p x) N
source
@[simp]
theorem MeasurableSet.disjointed {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → Set α} (h : ∀ (i : ℕ), MeasurableSet (f i)) (n : ℕ) :
MeasurableSet (disjointed f n)
source
theorem measurable_find {α : Type u_1} {mα : MeasurableSpace α} {p : α → ℕ → Prop} [(x : α) → DecidablePred (p x)] (hp : ∀ (x : α), ∃ (N : ℕ), p x N) (hm : ∀ (k : ℕ), MeasurableSet {x : α | p x k}) :
Measurable fun (x : α) => Nat.find ⋯
source
instance Quot.instMeasurableSpace {α : Type u_6} {r : α → α → Prop} [m : MeasurableSpace α] :
MeasurableSpace (Quot r)
Equations

- Quot.instMeasurableSpace = MeasurableSpace.map (Quot.mk r) m

source
instance Quotient.instMeasurableSpace {α : Type u_6} {s : Setoid α} [m : MeasurableSpace α] :
MeasurableSpace (Quotient s)
Equations

- Quotient.instMeasurableSpace = MeasurableSpace.map Quotient.mk'' m

source
instance QuotientGroup.measurableSpace {G : Type u_6} [Group G] [MeasurableSpace G] (S : Subgroup G) :
MeasurableSpace (G ⧸ S)
Equations

- QuotientGroup.measurableSpace S = Quotient.instMeasurableSpace

source
instance QuotientAddGroup.measurableSpace {G : Type u_6} [AddGroup G] [MeasurableSpace G] (S : AddSubgroup G) :
MeasurableSpace (G ⧸ S)
Equations

- QuotientAddGroup.measurableSpace S = Quotient.instMeasurableSpace

source
theorem measurableSet_quotient {α : Type u_1} [MeasurableSpace α] {s : Setoid α} {t : Set (Quotient s)} :
MeasurableSet t ↔ MeasurableSet (Quotient.mk'' ⁻¹' t)
source
theorem measurable_from_quotient {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {s : Setoid α} {f : Quotient s → β} :
Measurable f ↔ Measurable (f ∘ Quotient.mk'')
source
theorem measurable_quotient_mk' {α : Type u_1} [MeasurableSpace α] [s : Setoid α] :
Measurable Quotient.mk'
source
theorem measurable_quotient_mk'' {α : Type u_1} [MeasurableSpace α] {s : Setoid α} :
Measurable Quotient.mk''
source
theorem measurable_quot_mk {α : Type u_1} [MeasurableSpace α] {r : α → α → Prop} :
Measurable (Quot.mk r)
source
theorem QuotientGroup.measurable_coe {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} :
Measurable mk
source
theorem QuotientAddGroup.measurable_coe {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} :
Measurable mk
source
theorem QuotientGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} {f : G ⧸ S → α} :
Measurable f ↔ Measurable (f ∘ mk)
source
theorem QuotientAddGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} {f : G ⧸ S → α} :
Measurable f ↔ Measurable (f ∘ mk)
source
instance Quotient.instDiscreteMeasurableSpace {α : Type u_6} {s : Setoid α} [MeasurableSpace α] [DiscreteMeasurableSpace α] :
DiscreteMeasurableSpace (Quotient s)
source
instance QuotientGroup.instDiscreteMeasurableSpace {G : Type u_6} [Group G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (S : Subgroup G) :
DiscreteMeasurableSpace (G ⧸ S)
source
instance QuotientAddGroup.instDiscreteMeasurableSpace {G : Type u_6} [AddGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (S : AddSubgroup G) :
DiscreteMeasurableSpace (G ⧸ S)
source
instance Subtype.instMeasurableSpace {α : Type u_6} {p : α → Prop} [m : MeasurableSpace α] :
MeasurableSpace (Subtype p)
Equations

- Subtype.instMeasurableSpace = MeasurableSpace.comap Subtype.val m

source
theorem measurable_subtype_coe {α : Type u_1} [MeasurableSpace α] {p : α → Prop} :
Measurable Subtype.val
source
instance Subtype.instMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] {p : α → Prop} [MeasurableSingletonClass α] :
MeasurableSingletonClass (Subtype p)
source
theorem MeasurableSet.of_subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set ↑s} (h : MeasurableSet (Subtype.val '' t)) :
MeasurableSet t
source
theorem MeasurableSet.subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set ↑s} (hs : MeasurableSet s) :
MeasurableSet t → MeasurableSet (Subtype.val '' t)
source
theorem Measurable.subtype_coe {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → Subtype p} (hf : Measurable f) :
Measurable fun (a : α) => ↑(f a)
source
theorem Measurable.subtype_val {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → Subtype p} (hf : Measurable f) :
Measurable fun (a : α) => ↑(f a)

Alias of `Measurable.subtype_coe`.

source
theorem Measurable.subtype_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → β} (hf : Measurable f) {h : ∀ (x : α), p (f x)} :
Measurable fun (x : α) => ⟨f x, ⋯⟩
source
theorem Measurable.rangeFactorization {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) :
Measurable (Set.rangeFactorization f)
source
theorem Measurable.subtype_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {p : α → Prop} {q : β → Prop} (hf : Measurable f) (hpq : ∀ (x : α), p x → q (f x)) :
Measurable (Subtype.map f hpq)
source
theorem measurable_inclusion {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (h : s ⊆ t) :
Measurable (Set.inclusion h)
source
theorem MeasurableSet.image_inclusion' {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (h : s ⊆ t) {u : Set ↑s} (hs : MeasurableSet (Subtype.val ⁻¹' s)) (hu : MeasurableSet u) :
MeasurableSet (Set.inclusion h '' u)
source
theorem MeasurableSet.image_inclusion {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (h : s ⊆ t) {u : Set ↑s} (hs : MeasurableSet s) (hu : MeasurableSet u) :
MeasurableSet (Set.inclusion h '' u)
source
theorem MeasurableSet.of_union_cover {α : Type u_1} {m : MeasurableSpace α} {s t u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ ⊆ s ∪ t) (hsu : MeasurableSet (Subtype.val ⁻¹' u)) (htu : MeasurableSet (Subtype.val ⁻¹' u)) :
MeasurableSet u
source
theorem measurable_of_measurable_union_cover {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (s t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ ⊆ s ∪ t) (hc : Measurable fun (a : ↑s) => f ↑a) (hd : Measurable fun (a : ↑t) => f ↑a) :
Measurable f
source
theorem measurable_of_restrict_of_restrict_compl {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {s : Set α} (hs : MeasurableSet s) (h₁ : Measurable (s.restrict f)) (h₂ : Measurable (s ᶜ.restrict f)) :
Measurable f
source
theorem Measurable.dite {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [(x : α) → Decidable (x ∈ s)] {f : ↑s → β} (hf : Measurable f) {g : ↑s ᶜ → β} (hg : Measurable g) (hs : MeasurableSet s) :
Measurable fun (x : α) => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩
source
theorem measurable_of_measurable_on_compl_finite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {f : α → β} (s : Set α) (hs : s.Finite) (hf : Measurable (s ᶜ.restrict f)) :
Measurable f
source
theorem measurable_of_measurable_on_compl_singleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {f : α → β} (a : α) (hf : Measurable ({x : α | x ≠ a}.restrict f)) :
Measurable f
source
def measurableAtom {β : Type u_2} [MeasurableSpace β] (x : β) :
Set β

The measurable atom of `x` is the intersection of all the measurable sets containing `x`. It is measurable when the space is countable (or more generally when the measurable space is countably generated).

Equations

- measurableAtom x = ⋂ (s : Set β), ⋂ (_ : x ∈ s), ⋂ (_ : MeasurableSet s), s

Instances For

source
@[simp]
theorem mem_measurableAtom_self {β : Type u_2} [MeasurableSpace β] (x : β) :
x ∈ measurableAtom x
source
theorem mem_of_mem_measurableAtom {β : Type u_2} [MeasurableSpace β] {x y : β} (h : y ∈ measurableAtom x) {s : Set β} (hs : MeasurableSet s) (hxs : x ∈ s) :
y ∈ s
source
theorem measurableAtom_subset {β : Type u_2} [MeasurableSpace β] {s : Set β} {x : β} (hs : MeasurableSet s) (hx : x ∈ s) :
measurableAtom x ⊆ s
source
@[simp]
theorem measurableAtom_of_measurableSingletonClass {β : Type u_2} [MeasurableSpace β] [MeasurableSingletonClass β] (x : β) :
measurableAtom x = {x}
source
theorem MeasurableSet.measurableAtom_of_countable {β : Type u_2} [MeasurableSpace β] [Countable β] (x : β) :
MeasurableSet (measurableAtom x)
source
theorem measurableAtom_subset_of_mem {β : Type u_2} [MeasurableSpace β] {x y : β} (hx : x ∈ measurableAtom y) :
measurableAtom x ⊆ measurableAtom y

There is in fact equality: see `measurableAtom_eq_of_mem`.

source
theorem measurableAtom_eq_of_mem {β : Type u_2} [MeasurableSpace β] {x y : β} (hx : x ∈ measurableAtom y) :
measurableAtom x = measurableAtom y
source
theorem disjoint_measurableAtom_of_notMem {β : Type u_2} [MeasurableSpace β] {x y : β} (hx : x ∉ measurableAtom y) :
Disjoint (measurableAtom x) (measurableAtom y)
source
def MeasurableSpace.prod {α : Type u_6} {β : Type u_7} (m₁ : MeasurableSpace α) (m₂ : MeasurableSpace β) :
MeasurableSpace (α × β)

A `MeasurableSpace` structure on the product of two measurable spaces.

Equations

- m₁.prod m₂ = MeasurableSpace.comap Prod.fst m₁ ⊔ MeasurableSpace.comap Prod.snd m₂

Instances For

source
instance Prod.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :
MeasurableSpace (α × β)
Equations

- Prod.instMeasurableSpace = m₁.prod m₂

source
theorem measurable_fst {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} :
Measurable Prod.fst
source
theorem measurable_snd {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} :
Measurable Prod.snd
source
theorem Measurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} (hf : Measurable f) :
Measurable fun (a : α) => (f a).1
source
theorem Measurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} (hf : Measurable f) :
Measurable fun (a : α) => (f a).2
source
theorem Measurable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} (hf₁ : Measurable fun (a : α) => (f a).1) (hf₂ : Measurable fun (a : α) => (f a).2) :
Measurable f
source
theorem Measurable.prodMk {α : Type u_1} {m : MeasurableSpace α} {β : Type u_6} {γ : Type u_7} {x✝ : MeasurableSpace β} {x✝¹ : MeasurableSpace γ} {f : α → β} {g : α → γ} (hf : Measurable f) (hg : Measurable g) :
Measurable fun (a : α) => (f a, g a)
source
theorem Measurable.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) :
Measurable (Prod.map f g)
source
theorem measurable_prodMk_left {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α} :
Measurable (Prod.mk x)
source
theorem measurable_prodMk_right {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {y : β} :
Measurable fun (x : α) => (x, y)
source
theorem Measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β → γ} (hf : Measurable (Function.uncurry f)) {x : α} :
Measurable (f x)
source
theorem Measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β → γ} (hf : Measurable (Function.uncurry f)) {y : β} :
Measurable fun (x : α) => f x y
source
theorem measurable_fun_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} :
Measurable f ↔ (Measurable fun (a : α) => (f a).1) ∧ Measurable fun (a : α) => (f a).2
source
theorem measurable_swap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
Measurable Prod.swap
source
theorem measurable_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x✝ : MeasurableSpace γ} {f : α × β → γ} :
Measurable (f ∘ Prod.swap) ↔ Measurable f
source
theorem MeasurableSet.prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) :
MeasurableSet (s ×ˢ t)
source
theorem measurableSet_prod_of_nonempty {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (h : (s ×ˢ t).Nonempty) :
MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
source
theorem measurableSet_prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} :
MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
source
theorem measurableSet_swap_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α × β)} :
MeasurableSet (Prod.swap ⁻¹' s) ↔ MeasurableSet s
source
instance Prod.instMeasurableSingletonClass {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] [MeasurableSingletonClass β] :
MeasurableSingletonClass (α × β)
source
theorem measurable_from_prod_countable_left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Countable β] {f : α × β → γ} (hf : ∀ (y : β), Measurable fun (x : α) => f (x, y)) (h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)) :
Measurable f

See `measurable_from_prod_countable_left` for a version where we assume that singletons are measurable instead of reasoning about `measurableAtom`.

source
theorem measurable_from_prod_countable_right' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Countable α] {f : α × β → γ} (hf : ∀ (x : α), Measurable fun (y : β) => f (x, y)) (h'f : ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)) :
Measurable f

See `measurable_from_prod_countable_right` for a version where we assume that singletons are measurable instead of reasoning about `measurableAtom`.

source
@[deprecated measurable_from_prod_countable_left' (since := "2025-08-17")]
theorem measurable_from_prod_countable' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Countable β] {f : α × β → γ} (hf : ∀ (y : β), Measurable fun (x : α) => f (x, y)) (h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)) :
Measurable f

Alias of `measurable_from_prod_countable_left'`.

See `measurable_from_prod_countable_left` for a version where we assume that singletons are measurable instead of reasoning about `measurableAtom`.

source
theorem measurable_from_prod_countable_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Countable β] [MeasurableSingletonClass β] {f : α × β → γ} (hf : ∀ (y : β), Measurable fun (x : α) => f (x, y)) :
Measurable f

For the version where the first space in the product is countable, see `measurable_from_prod_countable_right`.

source
theorem measurable_from_prod_countable_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Countable α] [MeasurableSingletonClass α] {f : α × β → γ} (hf : ∀ (x : α), Measurable fun (y : β) => f (x, y)) :
Measurable f

For the version where the second space in the product is countable, see `measurable_from_prod_countable_left`.

source
theorem Measurable.find {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {x✝ : MeasurableSpace α} {f : ℕ → α → β} {p : ℕ → α → Prop} [(n : ℕ) → DecidablePred (p n)] (hf : ∀ (n : ℕ), Measurable (f n)) (hp : ∀ (n : ℕ), MeasurableSet {x : α | p n x}) (h : ∀ (x : α), ∃ (n : ℕ), p n x) :
Measurable fun (x : α) => f (Nat.find ⋯) x

A piecewise function on countably many pieces is measurable if all the data is measurable.

source
theorem measurable_iUnionLift {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] {t : ι → Set α} {f : (i : ι) → ↑(t i) → β} (htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) {T : Set α} (hT : T ⊆ ⋃ (i : ι), t i) (htm : ∀ (i : ι), MeasurableSet (t i)) (hfm : ∀ (i : ι), Measurable (f i)) :
Measurable (Set.iUnionLift t f htf T hT)

Let `t i` be a countable covering of a set `T` by measurable sets. Let `f i : t i → β` be a family of functions that agree on the intersections `t i ∩ t j`. Then the function `Set.iUnionLift t f _ _ : T → β`, defined as `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable.

source
theorem measurable_liftCover {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (t : ι → Set α) (htm : ∀ (i : ι), MeasurableSet (t i)) (f : (i : ι) → ↑(t i) → β) (hfm : ∀ (i : ι), Measurable (f i)) (hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) (htU : ⋃ (i : ι), t i = Set.univ) :
Measurable (Set.liftCover t f hf htU)

Let `t i` be a countable covering of `α` by measurable sets. Let `f i : t i → β` be a family of functions that agree on the intersections `t i ∩ t j`. Then the function `Set.liftCover t f _ _`, defined as `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable.

source
theorem exists_measurable_piecewise {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {ι : Type u_6} [Countable ι] [Nonempty ι] (t : ι → Set α) (t_meas : ∀ (n : ι), MeasurableSet (t n)) (g : ι → α → β) (hg : ∀ (n : ι), Measurable (g n)) (ht : Pairwise fun (i j : ι) => Set.EqOn (g i) (g j) (t i ∩ t j)) :
∃ (f : α → β), Measurable f ∧ ∀ (n : ι), Set.EqOn f (g n) (t n)

Let `t i` be a nonempty countable family of measurable sets in `α`. Let `g i : α → β` be a family of measurable functions such that `g i` agrees with `g j` on `t i ∩ t j`. Then there exists a measurable function `f : α → β` that agrees with each `g i` on `t i`.

We only need the assumption `[Nonempty ι]` to prove `[Nonempty (α → β)]`.

source
instance MeasurableSpace.pi {δ : Type u_4} {X : δ → Type u_6} [m : (a : δ) → MeasurableSpace (X a)] :
MeasurableSpace ((a : δ) → X a)
Equations

- MeasurableSpace.pi = ⨆ (a : δ), MeasurableSpace.comap (fun (b : (a : δ) → X a) => b a) (m a)

source
theorem measurable_pi_iff {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (X a)] {g : α → (a : δ) → X a} :
Measurable g ↔ ∀ (a : δ), Measurable fun (x : α) => g x a
source
theorem measurable_pi_apply {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] (a : δ) :
Measurable fun (f : (a : δ) → X a) => f a
source
theorem Measurable.eval {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (X a)] {a : δ} {g : α → (a : δ) → X a} (hg : Measurable g) :
Measurable fun (x : α) => g x a
source
theorem measurable_pi_lambda {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (X a)] (f : α → (a : δ) → X a) (hf : ∀ (a : δ), Measurable fun (c : α) => f c a) :
Measurable f
source
theorem measurable_update' {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] {a : δ} [DecidableEq δ] :
Measurable fun (p : ((i : δ) → X i) × X a) => Function.update p.1 a p.2

The function `(f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a` is measurable.

source
theorem measurable_uniqueElim {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] [Unique δ] :
Measurable uniqueElim
source
theorem measurable_updateFinset' {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] [DecidableEq δ] {s : Finset δ} :
Measurable fun (p : ((i : δ) → X i) × ((i : ↥s) → X ↑i)) => Function.updateFinset p.1 s p.2
source
theorem measurable_updateFinset {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] [DecidableEq δ] {s : Finset δ} {x : (i : δ) → X i} :
Measurable (Function.updateFinset x s)
source
theorem measurable_updateFinset_left {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] [DecidableEq δ] {s : Finset δ} {x : (i : ↥s) → X ↑i} :
Measurable fun (x_1 : (i : δ) → X i) => Function.updateFinset x_1 s x
source
theorem measurable_update {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] (f : (a : δ) → X a) {a : δ} [DecidableEq δ] :
Measurable (Function.update f a)

The function `update f a : X a → Π a, X a` is always measurable. This doesn't require `f` to be measurable. This should not be confused with the statement that `update f a x` is measurable.

source
theorem measurable_update_left {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] {a : δ} [DecidableEq δ] {x : X a} :
Measurable fun (x_1 : (a : δ) → X a) => Function.update x_1 a x
source
theorem Set.measurable_restrict {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] (s : Set δ) :
Measurable s.restrict
source
theorem Set.measurable_restrict₂ {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] {s t : Set δ} (hst : s ⊆ t) :
Measurable (restrict₂ hst)
source
theorem Finset.measurable_restrict {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] (s : Finset δ) :
Measurable s.restrict
source
theorem Finset.measurable_restrict₂ {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] {s t : Finset δ} (hst : s ⊆ t) :
Measurable (restrict₂ hst)
source
theorem Set.measurable_restrict_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] (s : Set α) {f : α → γ} (hf : Measurable f) :
Measurable (s.restrict f)
source
theorem Set.measurable_restrict₂_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] {s t : Set α} (hst : s ⊆ t) {f : ↑t → γ} (hf : Measurable f) :
Measurable (restrict₂ hst f)
source
theorem Finset.measurable_restrict_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] (s : Finset α) {f : α → γ} (hf : Measurable f) :
Measurable (s.restrict f)
source
theorem Finset.measurable_restrict₂_apply {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] {s t : Finset α} (hst : s ⊆ t) {f : ↥t → γ} (hf : Measurable f) :
Measurable (restrict₂ hst f)
source
theorem measurable_eq_mp {δ : Type u_4} (X : δ → Type u_6) [(a : δ) → MeasurableSpace (X a)] {i i' : δ} (h : i = i') :
Measurable ⋯.mp
source
theorem Measurable.eq_mp {δ : Type u_4} (X : δ → Type u_6) [(a : δ) → MeasurableSpace (X a)] {β : Type u_7} [MeasurableSpace β] {i i' : δ} (h : i = i') {f : β → X i} (hf : Measurable f) :
Measurable fun (x : β) => ⋯.mp (f x)
source
theorem measurable_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] (f : δ' ≃ δ) :
Measurable ⇑(Equiv.piCongrLeft X f)
source
theorem MeasurableSet.pi {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] {s : Set δ} {t : (i : δ) → Set (X i)} (hs : s.Countable) (ht : ∀ i ∈ s, MeasurableSet (t i)) :
MeasurableSet (s.pi t)
source
theorem MeasurableSet.univ_pi {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] [Countable δ] {t : (i : δ) → Set (X i)} (ht : ∀ (i : δ), MeasurableSet (t i)) :
MeasurableSet (Set.univ.pi t)
source
theorem measurableSet_pi_of_nonempty {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] {s : Set δ} {t : (i : δ) → Set (X i)} (hs : s.Countable) (h : (s.pi t).Nonempty) :
MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)
source
theorem measurableSet_pi {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] {s : Set δ} {t : (i : δ) → Set (X i)} (hs : s.Countable) :
MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
source
instance Pi.instMeasurableSingletonClass {δ : Type u_4} {X : δ → Type u_6} [(a : δ) → MeasurableSpace (X a)] [Countable δ] [∀ (a : δ), MeasurableSingletonClass (X a)] :
MeasurableSingletonClass ((a : δ) → X a)
source
theorem measurable_piEquivPiSubtypeProd_symm {δ : Type u_4} (X : δ → Type u_6) [(a : δ) → MeasurableSpace (X a)] (p : δ → Prop) [DecidablePred p] :
Measurable ⇑(Equiv.piEquivPiSubtypeProd p X).symm
source
theorem measurable_piEquivPiSubtypeProd {δ : Type u_4} (X : δ → Type u_6) [(a : δ) → MeasurableSpace (X a)] (p : δ → Prop) [DecidablePred p] :
Measurable ⇑(Equiv.piEquivPiSubtypeProd p X)
source
instance TProd.instMeasurableSpace {δ : Type u_4} (X : δ → Type u_6) [(i : δ) → MeasurableSpace (X i)] (l : List δ) :
MeasurableSpace (List.TProd X l)
Equations

- TProd.instMeasurableSpace X [] = PUnit.instMeasurableSpace
- TProd.instMeasurableSpace X (head :: is) = Prod.instMeasurableSpace

source
theorem measurable_tProd_mk {δ : Type u_4} {X : δ → Type u_6} [(i : δ) → MeasurableSpace (X i)] (l : List δ) :
Measurable (List.TProd.mk l)
source
theorem measurable_tProd_elim {δ : Type u_4} {X : δ → Type u_6} [(i : δ) → MeasurableSpace (X i)] [DecidableEq δ] {l : List δ} {i : δ} (hi : i ∈ l) :
Measurable fun (v : List.TProd X l) => v.elim hi
source
theorem measurable_tProd_elim' {δ : Type u_4} {X : δ → Type u_6} [(i : δ) → MeasurableSpace (X i)] [DecidableEq δ] {l : List δ} (h : ∀ (i : δ), i ∈ l) :
Measurable (List.TProd.elim' h)
source
theorem MeasurableSet.tProd {δ : Type u_4} {X : δ → Type u_6} [(i : δ) → MeasurableSpace (X i)] (l : List δ) {s : (i : δ) → Set (X i)} (hs : ∀ (i : δ), MeasurableSet (s i)) :
MeasurableSet (Set.tprod l s)
source
instance Sum.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :
MeasurableSpace (α ⊕ β)
Equations

- Sum.instMeasurableSpace = MeasurableSpace.map Sum.inl m₁ ⊓ MeasurableSpace.map Sum.inr m₂

source
theorem measurable_inl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
Measurable Sum.inl
source
theorem measurable_inr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
Measurable Sum.inr
source
theorem measurableSet_sum_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α ⊕ β)} :
MeasurableSet s ↔ MeasurableSet (Sum.inl ⁻¹' s) ∧ MeasurableSet (Sum.inr ⁻¹' s)
source
theorem measurable_fun_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x✝ : MeasurableSpace γ} {f : α ⊕ β → γ} (hl : Measurable (f ∘ Sum.inl)) (hr : Measurable (f ∘ Sum.inr)) :
Measurable f
source
theorem Measurable.sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x✝ : MeasurableSpace γ} {f : α → γ} {g : β → γ} (hf : Measurable f) (hg : Measurable g) :
Measurable (Sum.elim f g)
source
theorem Measurable.sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x✝ : MeasurableSpace γ} {x✝¹ : MeasurableSpace δ} {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) :
Measurable (Sum.map f g)
source
@[simp]
theorem measurableSet_inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :
MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s
source
theorem MeasurableSet.inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :
MeasurableSet s → MeasurableSet (Sum.inl '' s)

Alias of the reverse direction of `measurableSet_inl_image`.

source
@[simp]
theorem measurableSet_inr_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} :
MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s
source
theorem MeasurableSet.inr_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} :
MeasurableSet s → MeasurableSet (Sum.inr '' s)

Alias of the reverse direction of `measurableSet_inr_image`.

source
theorem measurableSet_range_inl {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace α] :
MeasurableSet (Set.range Sum.inl)
source
theorem measurableSet_range_inr {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace α] :
MeasurableSet (Set.range Sum.inr)
source
instance Sigma.instMeasurableSpace {α : Type u_7} {β : α → Type u_6} [m : (a : α) → MeasurableSpace (β a)] :
MeasurableSpace (Sigma β)
Equations

- Sigma.instMeasurableSpace = ⨅ (a : α), MeasurableSpace.map (Sigma.mk a) (m a)

source
@[simp]
theorem measurableSet_setOf {α : Type u_1} [MeasurableSpace α] {p : α → Prop} :
MeasurableSet {a : α | p a} ↔ Measurable p
source
@[simp]
theorem measurable_mem {α : Type u_1} {s : Set α} [MeasurableSpace α] :
(Measurable fun (x : α) => x ∈ s) ↔ MeasurableSet s
source
theorem Measurable.setOf {α : Type u_1} [MeasurableSpace α] {p : α → Prop} :
Measurable p → MeasurableSet {a : α | p a}

Alias of the reverse direction of `measurableSet_setOf`.

source
theorem MeasurableSet.mem {α : Type u_1} {s : Set α} [MeasurableSpace α] :
MeasurableSet s → Measurable fun (x : α) => x ∈ s

Alias of the reverse direction of `measurable_mem`.

source
theorem Measurable.not {α : Type u_1} [MeasurableSpace α] {p : α → Prop} (hp : Measurable p) :
Measurable fun (x : α) => ¬p x
source
theorem Measurable.and {α : Type u_1} [MeasurableSpace α] {p q : α → Prop} (hp : Measurable p) (hq : Measurable q) :
Measurable fun (a : α) => p a ∧ q a
source
theorem Measurable.or {α : Type u_1} [MeasurableSpace α] {p q : α → Prop} (hp : Measurable p) (hq : Measurable q) :
Measurable fun (a : α) => p a ∨ q a
source
theorem Measurable.imp {α : Type u_1} [MeasurableSpace α] {p q : α → Prop} (hp : Measurable p) (hq : Measurable q) :
Measurable fun (a : α) => p a → q a
source
theorem Measurable.iff {α : Type u_1} [MeasurableSpace α] {p q : α → Prop} (hp : Measurable p) (hq : Measurable q) :
Measurable fun (a : α) => p a ↔ q a
source
theorem Measurable.forall {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] [Countable ι] {p : ι → α → Prop} (hp : ∀ (i : ι), Measurable (p i)) :
Measurable fun (a : α) => ∀ (i : ι), p i a
source
theorem Measurable.exists {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] [Countable ι] {p : ι → α → Prop} (hp : ∀ (i : ι), Measurable (p i)) :
Measurable fun (a : α) => ∃ (i : ι), p i a
source
instance Set.instMeasurableSpace {α : Type u_1} :
MeasurableSpace (Set α)

This instance is useful when talking about Bernoulli sequences of random variables or binomial random graphs.

Equations

- Set.instMeasurableSpace = id inferInstance

source
instance Set.instMeasurableSingletonClass {α : Type u_1} [Countable α] :
MeasurableSingletonClass (Set α)
source
theorem measurable_set_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {g : β → Set α} :
Measurable g ↔ ∀ (a : α), Measurable fun (x : β) => a ∈ g x
source
theorem measurable_set_mem {α : Type u_1} (a : α) :
Measurable fun (s : Set α) => a ∈ s
source
theorem measurable_set_notMem {α : Type u_1} (a : α) :
Measurable fun (s : Set α) => a ∉ s
source
@[deprecated measurable_set_notMem (since := "2025-05-23")]
theorem measurable_set_not_mem {α : Type u_1} (a : α) :
Measurable fun (s : Set α) => a ∉ s

Alias of `measurable_set_notMem`.

source
theorem measurableSet_mem {α : Type u_1} (a : α) :
MeasurableSet {s : Set α | a ∈ s}
source
theorem measurableSet_notMem {α : Type u_1} (a : α) :
MeasurableSet {s : Set α | a ∉ s}
source
@[deprecated measurableSet_notMem (since := "2025-05-23")]
theorem measurableSet_not_mem {α : Type u_1} (a : α) :
MeasurableSet {s : Set α | a ∉ s}

Alias of `measurableSet_notMem`.

source
theorem measurable_compl {α : Type u_1} :
Measurable fun (x : Set α) => x ᶜ
source
theorem MeasurableSet.setOf_finite {α : Type u_1} [Countable α] :
MeasurableSet {s : Set α | s.Finite}
source
theorem MeasurableSet.setOf_infinite {α : Type u_1} [Countable α] :
MeasurableSet {s : Set α | s.Infinite}
source
theorem MeasurableSet.sep_finite {α : Type u_1} [Countable α] {S : Set (Set α)} (hS : MeasurableSet S) :
MeasurableSet {s : Set α | s ∈ S ∧ s.Finite}
source
theorem MeasurableSet.sep_infinite {α : Type u_1} [Countable α] {S : Set (Set α)} (hS : MeasurableSet S) :
MeasurableSet {s : Set α | s ∈ S ∧ s.Infinite}
source
theorem measurable_curry {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [MeasurableSpace X] :
Measurable Function.curry
source
theorem measurable_uncurry {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [MeasurableSpace X] :
Measurable Function.uncurry
source
theorem measurable_equivCurry {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [MeasurableSpace X] :
Measurable ⇑(Equiv.curry ι κ X)
source
theorem measurable_equivCurry_symm {ι : Type u_6} {κ : Type u_7} {X : Type u_8} [MeasurableSpace X] :
Measurable ⇑(Equiv.curry ι κ X).symm
source
theorem measurable_sigmaCurry {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8} [(i : ι) → (j : κ i) → MeasurableSpace (X i j)] :
Measurable Sigma.curry
source
theorem measurable_sigmaUncurry {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8} [(i : ι) → (j : κ i) → MeasurableSpace (X i j)] :
Measurable Sigma.uncurry
source
theorem measurable_piCurry {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8} [(i : ι) → (j : κ i) → MeasurableSpace (X i j)] :
Measurable ⇑(Equiv.piCurry X)
source
theorem measurable_piCurry_symm {ι : Type u_6} {κ : ι → Type u_7} {X : (i : ι) → κ i → Type u_8} [(i : ι) → (j : κ i) → MeasurableSpace (X i j)] :
Measurable ⇑(Equiv.piCurry X).symm