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.
theorem
measurable_to_countable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[Countable α]
[MeasurableSpace β]
{f : β → α}
(h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y}))
:
theorem
measurable_to_countable'
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[Countable α]
[MeasurableSpace β]
{f : β → α}
(h : ∀ (x : α), MeasurableSet (f ⁻¹' {x}))
:
theorem
ENat.measurable_iff
{α : Type u_6}
[MeasurableSpace α]
{f : α → ℕ∞}
:
Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
@[implicit_reducible]
instance
ULift.instMeasurableSpace
{α : Type u_1}
[MeasurableSpace α]
:
MeasurableSpace (ULift.{u_6, u_1} α)
@[simp]
theorem
measurableSet_preimage_down
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
:
MeasurableSet (ULift.down ⁻¹' s) ↔ MeasurableSet s
@[simp]
theorem
measurableSet_preimage_up
{α : Type u_1}
[MeasurableSpace α]
{s : Set (ULift.{u_6, u_1} α)}
:
MeasurableSet (ULift.up ⁻¹' s) ↔ MeasurableSet s
theorem
measurable_to_nat
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℕ}
:
(∀ (y : α), MeasurableSet (f ⁻¹' {f y})) → Measurable f
theorem
measurable_to_bool
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → Bool}
(h : MeasurableSet (f ⁻¹' {true}))
:
theorem
measurable_to_prop
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → Prop}
(h : MeasurableSet (f ⁻¹' {True}))
:
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
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
@[simp]
theorem
MeasurableSet.disjointed
{α : Type u_1}
{mα : MeasurableSpace α}
{f : ℕ → Set α}
(h : ∀ (i : ℕ), MeasurableSet (f i))
(n : ℕ)
:
MeasurableSet (disjointed f n)
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 ⋯
@[implicit_reducible]
instance
Quot.instMeasurableSpace
{α : Type u_6}
{r : α → α → Prop}
[m : MeasurableSpace α]
:
MeasurableSpace (Quot r)
@[implicit_reducible]
instance
Quotient.instMeasurableSpace
{α : Type u_6}
{s : Setoid α}
[m : MeasurableSpace α]
:
MeasurableSpace (Quotient s)
@[implicit_reducible]
instance
QuotientGroup.measurableSpace
{G : Type u_6}
[Group G]
[MeasurableSpace G]
(S : Subgroup G)
:
MeasurableSpace (G ⧸ S)
@[implicit_reducible]
instance
QuotientAddGroup.measurableSpace
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
(S : AddSubgroup G)
:
MeasurableSpace (G ⧸ S)
theorem
measurableSet_quotient
{α : Type u_1}
[MeasurableSpace α]
{s : Setoid α}
{t : Set (Quotient s)}
:
MeasurableSet t ↔ MeasurableSet (Quotient.mk'' ⁻¹' t)
theorem
measurable_from_quotient
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{s : Setoid α}
{f : Quotient s → β}
:
Measurable f ↔ Measurable (f ∘ Quotient.mk'')
theorem
measurable_quotient_mk'
{α : Type u_1}
[MeasurableSpace α]
[s : Setoid α]
:
Measurable Quotient.mk'
theorem
measurable_quot_mk
{α : Type u_1}
[MeasurableSpace α]
{r : α → α → Prop}
:
Measurable (Quot.mk r)
theorem
QuotientGroup.measurable_coe
{G : Type u_6}
[Group G]
[MeasurableSpace G]
{S : Subgroup G}
:
theorem
QuotientAddGroup.measurable_coe
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
{S : AddSubgroup G}
:
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)
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)
instance
Quotient.instDiscreteMeasurableSpace
{α : Type u_6}
{s : Setoid α}
[MeasurableSpace α]
[DiscreteMeasurableSpace α]
:
DiscreteMeasurableSpace (Quotient s)
instance
QuotientGroup.instDiscreteMeasurableSpace
{G : Type u_6}
[Group G]
[MeasurableSpace G]
[DiscreteMeasurableSpace G]
(S : Subgroup G)
:
DiscreteMeasurableSpace (G ⧸ S)
instance
QuotientAddGroup.instDiscreteMeasurableSpace
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
[DiscreteMeasurableSpace G]
(S : AddSubgroup G)
:
DiscreteMeasurableSpace (G ⧸ S)
@[implicit_reducible]
instance
Subtype.instMeasurableSpace
{α : Type u_6}
{p : α → Prop}
[m : MeasurableSpace α]
:
MeasurableSpace (Subtype p)
theorem
measurable_subtype_coe
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
:
Measurable Subtype.val
instance
Subtype.instMeasurableSingletonClass
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
[MeasurableSingletonClass α]
:
MeasurableSingletonClass (Subtype p)
theorem
MeasurableSet.of_subtype_image
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{t : Set ↑s}
(h : MeasurableSet (Subtype.val '' t))
:
theorem
MeasurableSet.subtype_image
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{t : Set ↑s}
(hs : MeasurableSet s)
:
MeasurableSet t → MeasurableSet (Subtype.val '' t)
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)
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.
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, ⋯⟩
theorem
Measurable.codRestrict
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
{f : α → β}
(hf : Measurable f)
(h : ∀ (y : α), f y ∈ s)
:
Measurable (Set.codRestrict f s h)
theorem
Measurable.rangeFactorization
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
:
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)
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)
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)
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))
:
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)
:
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))
:
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⟩
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))
:
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))
:
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).
Instances For
@[simp]
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
theorem
measurableAtom_subset
{β : Type u_2}
[MeasurableSpace β]
{s : Set β}
{x : β}
(hs : MeasurableSet s)
(hx : x ∈ s)
:
measurableAtom x ⊆ s
@[simp]
theorem
measurableAtom_of_measurableSingletonClass
{β : Type u_2}
[MeasurableSpace β]
[MeasurableSingletonClass β]
(x : β)
:
measurableAtom x = {x}
theorem
MeasurableSet.measurableAtom_of_countable
{β : Type u_2}
[MeasurableSpace β]
[Countable β]
(x : β)
:
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.
theorem
measurableAtom_eq_of_mem
{β : Type u_2}
[MeasurableSpace β]
{x y : β}
(hx : x ∈ measurableAtom y)
:
measurableAtom x = measurableAtom y
theorem
disjoint_measurableAtom_of_notMem
{β : Type u_2}
[MeasurableSpace β]
{x y : β}
(hx : x ∉ measurableAtom y)
:
Disjoint (measurableAtom x) (measurableAtom y)
@[implicit_reducible]
def
MeasurableSpace.prod
{α : Type u_6}
{β : Type u_7}
(m₁ : MeasurableSpace α)
(m₂ : MeasurableSpace β)
:
MeasurableSpace (α × β)
A MeasurableSpace structure on the product of two measurable spaces.
Instances For
@[implicit_reducible]
instance
Prod.instMeasurableSpace
{α : Type u_6}
{β : Type u_7}
[m₁ : MeasurableSpace α]
[m₂ : MeasurableSpace β]
:
MeasurableSpace (α × β)
theorem
measurable_fst
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
:
theorem
measurable_snd
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
:
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
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
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)
:
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)
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)
theorem
measurable_prodMk_left
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{x : α}
:
Measurable (Prod.mk x)
theorem
measurable_prodMk_right
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{y : β}
:
Measurable fun (x : α) => (x, y)
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)
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
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
theorem
measurable_swap
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
:
Measurable Prod.swap
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
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)
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
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 = ∅
theorem
measurableSet_swap_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set (α × β)}
:
MeasurableSet (Prod.swap ⁻¹' s) ↔ MeasurableSet s
instance
Prod.instMeasurableSingletonClass
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
:
MeasurableSingletonClass (α × β)
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))
:
See measurable_from_prod_countable_left for a version where we assume that singletons are
measurable instead of reasoning about measurableAtom.
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))
:
See measurable_from_prod_countable_right for a version where we assume that singletons are
measurable instead of reasoning about measurableAtom.
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))
:
For the version where the first space in the product is countable,
see measurable_from_prod_countable_right.
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))
:
For the version where the second space in the product is countable,
see measurable_from_prod_countable_left.
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.
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.
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.
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 (α → β)].
@[implicit_reducible]
instance
MeasurableSpace.pi
{δ : Type u_4}
{X : δ → Type u_6}
[m : (a : δ) → MeasurableSpace (X a)]
:
MeasurableSpace ((a : δ) → X a)
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
theorem
measurable_pi_apply
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
(a : δ)
:
Measurable fun (f : (a : δ) → X a) => f a
theorem
MeasurableSpace.comap_le_comap_pi
{β : Type u_2}
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
{g : (a : δ) → β → X a}
(a : δ)
:
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
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)
:
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.
theorem
measurable_uniqueElim
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
[Unique δ]
:
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
theorem
measurable_updateFinset
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
[DecidableEq δ]
{s : Finset δ}
{x : (i : δ) → X i}
:
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
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.
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
theorem
Set.measurable_restrict
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
(s : Set δ)
:
theorem
Set.measurable_restrict₂
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
{s t : Set δ}
(hst : s ⊆ t)
:
Measurable (restrict₂ hst)
theorem
Finset.measurable_restrict
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
(s : Finset δ)
:
theorem
Finset.measurable_restrict₂
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
{s t : Finset δ}
(hst : s ⊆ t)
:
Measurable (restrict₂ hst)
theorem
Set.measurable_restrict_apply
{α : Type u_1}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
(s : Set α)
{f : α → γ}
(hf : Measurable f)
:
Measurable (s.restrict f)
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)
theorem
Finset.measurable_restrict_apply
{α : Type u_1}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
(s : Finset α)
{f : α → γ}
(hf : Measurable f)
:
Measurable (s.restrict f)
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)
theorem
measurable_eq_mp
{δ : Type u_4}
(X : δ → Type u_6)
[(a : δ) → MeasurableSpace (X a)]
{i i' : δ}
(h : i = i')
:
Measurable ⋯.mp
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)
theorem
measurable_piCongrLeft
{δ : Type u_4}
{δ' : Type u_5}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
(f : δ' ≃ δ)
:
Measurable ⇑(Equiv.piCongrLeft X f)
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)
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)
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 {f : (i : δ) → X i | ∀ (i : δ), f i ∈ t i}
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)
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 = ∅
instance
Pi.instMeasurableSingletonClass
{δ : Type u_4}
{X : δ → Type u_6}
[(a : δ) → MeasurableSpace (X a)]
[Countable δ]
[∀ (a : δ), MeasurableSingletonClass (X a)]
:
MeasurableSingletonClass ((a : δ) → X a)
theorem
measurable_piEquivPiSubtypeProd_symm
{δ : Type u_4}
(X : δ → Type u_6)
[(a : δ) → MeasurableSpace (X a)]
(p : δ → Prop)
[DecidablePred p]
:
theorem
measurable_piEquivPiSubtypeProd
{δ : Type u_4}
(X : δ → Type u_6)
[(a : δ) → MeasurableSpace (X a)]
(p : δ → Prop)
[DecidablePred p]
:
@[implicit_reducible]
instance
TProd.instMeasurableSpace
{δ : Type u_4}
(X : δ → Type u_6)
[(i : δ) → MeasurableSpace (X i)]
(l : List δ)
:
MeasurableSpace (List.TProd X l)
theorem
measurable_tProd_mk
{δ : Type u_4}
{X : δ → Type u_6}
[(i : δ) → MeasurableSpace (X i)]
(l : List δ)
:
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
theorem
measurable_tProd_elim'
{δ : Type u_4}
{X : δ → Type u_6}
[(i : δ) → MeasurableSpace (X i)]
[DecidableEq δ]
{l : List δ}
(h : ∀ (i : δ), i ∈ l)
:
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)
@[implicit_reducible]
instance
Sum.instMeasurableSpace
{α : Type u_6}
{β : Type u_7}
[m₁ : MeasurableSpace α]
[m₂ : MeasurableSpace β]
:
MeasurableSpace (α ⊕ β)
theorem
measurable_inl
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
Measurable Sum.inl
theorem
measurable_inr
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
Measurable Sum.inr
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)
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))
:
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)
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)
@[simp]
theorem
measurableSet_inl_image
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set α}
:
MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s
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.
@[simp]
theorem
measurableSet_inr_image
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{s : Set β}
:
MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s
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.
theorem
measurableSet_range_inl
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace α]
:
MeasurableSet (Set.range Sum.inl)
theorem
measurableSet_range_inr
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
[MeasurableSpace α]
:
MeasurableSet (Set.range Sum.inr)
@[implicit_reducible]
instance
Sigma.instMeasurableSpace
{α : Type u_7}
{β : α → Type u_6}
[m : (a : α) → MeasurableSpace (β a)]
:
MeasurableSpace (Sigma β)
@[simp]
theorem
measurableSet_setOf
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
:
MeasurableSet {a : α | p a} ↔ Measurable p
@[simp]
theorem
measurable_mem
{α : Type u_1}
{s : Set α}
[MeasurableSpace α]
:
(Measurable fun (x : α) => x ∈ s) ↔ MeasurableSet s
theorem
Measurable.setOf
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
:
Measurable p → MeasurableSet {a : α | p a}
Alias of the reverse direction of measurableSet_setOf.
theorem
MeasurableSet.mem
{α : Type u_1}
{s : Set α}
[MeasurableSpace α]
:
MeasurableSet s → Measurable fun (x : α) => x ∈ s
Alias of the reverse direction of measurable_mem.
theorem
Measurable.not
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
(hp : Measurable p)
:
Measurable fun (x : α) => ¬p x
theorem
Measurable.and
{α : Type u_1}
[MeasurableSpace α]
{p q : α → Prop}
(hp : Measurable p)
(hq : Measurable q)
:
Measurable fun (a : α) => p a ∧ q a
theorem
Measurable.or
{α : Type u_1}
[MeasurableSpace α]
{p q : α → Prop}
(hp : Measurable p)
(hq : Measurable q)
:
Measurable fun (a : α) => p a ∨ q a
theorem
Measurable.imp
{α : Type u_1}
[MeasurableSpace α]
{p q : α → Prop}
(hp : Measurable p)
(hq : Measurable q)
:
Measurable fun (a : α) => p a → q a
theorem
Measurable.iff
{α : Type u_1}
[MeasurableSpace α]
{p q : α → Prop}
(hp : Measurable p)
(hq : Measurable q)
:
Measurable fun (a : α) => p a ↔ q a
theorem
Measurable.forall
{α : Type u_1}
{ι : Sort uι}
[MeasurableSpace α]
[Countable ι]
{p : ι → α → Prop}
(hp : ∀ (i : ι), Measurable (p i))
:
Measurable fun (a : α) => ∀ (i : ι), p i a
theorem
Measurable.exists
{α : Type u_1}
{ι : Sort uι}
[MeasurableSpace α]
[Countable ι]
{p : ι → α → Prop}
(hp : ∀ (i : ι), Measurable (p i))
:
Measurable fun (a : α) => ∃ (i : ι), p i a
theorem
Measurable.eq_const
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSingletonClass β]
{f : α → β}
(hf : Measurable f)
(a : β)
:
Measurable fun (x : α) => f x = a
theorem
Measurable.const_eq
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSingletonClass β]
{f : α → β}
(hf : Measurable f)
(a : β)
:
Measurable fun (x : α) => a = f x
@[implicit_reducible]
This instance is useful when talking about Bernoulli sequences of random variables or binomial random graphs.
@[simp]
theorem
measurable_set_iff
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace β]
{g : β → Set α}
:
Measurable g ↔ ∀ (a : α), Measurable fun (x : β) => a ∈ g x
theorem
MeasurableSet.sep_finite
{α : Type u_1}
[Countable α]
{S : Set (Set α)}
(hS : MeasurableSet S)
:
theorem
MeasurableSet.sep_infinite
{α : Type u_1}
[Countable α]
{S : Set (Set α)}
(hS : MeasurableSet S)
:
theorem
Measurable.subset
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace β]
[Countable α]
{s t : β → Set α}
(hs : Measurable s)
:
Measurable t → Measurable fun (a : β) => s a ⊆ t a
theorem
measurable_curry
{ι : Type u_6}
{κ : Type u_7}
{X : Type u_8}
[MeasurableSpace X]
:
Measurable Function.curry
theorem
measurable_uncurry
{ι : Type u_6}
{κ : Type u_7}
{X : Type u_8}
[MeasurableSpace X]
:
Measurable Function.uncurry
theorem
measurable_equivCurry
{ι : Type u_6}
{κ : Type u_7}
{X : Type u_8}
[MeasurableSpace X]
:
Measurable ⇑(Equiv.curry ι κ X)
theorem
measurable_equivCurry_symm
{ι : Type u_6}
{κ : Type u_7}
{X : Type u_8}
[MeasurableSpace X]
:
Measurable ⇑(Equiv.curry ι κ X).symm
theorem
measurable_sigmaCurry
{ι : Type u_6}
{κ : ι → Type u_7}
{X : (i : ι) → κ i → Type u_8}
[(i : ι) → (j : κ i) → MeasurableSpace (X i j)]
:
theorem
measurable_sigmaUncurry
{ι : Type u_6}
{κ : ι → Type u_7}
{X : (i : ι) → κ i → Type u_8}
[(i : ι) → (j : κ i) → MeasurableSpace (X i j)]
:
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)
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
Typeclass for a measurable space α for which the diagonal of α × α is measurable.
- measurableSet_diagonal : MeasurableSet (Set.diagonal α)
Instances
theorem
measurableSet_eq_fun
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableEq β]
{f g : α → β}
(hf : Measurable f)
(hg : Measurable g)
:
MeasurableSet {x : α | f x = g x}
theorem
Measurable.eq
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableEq β]
{f g : α → β}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (x : α) => f x = g x
instance
instMeasurableSingletonClassOfMeasurableEq
{α : Type u_1}
[MeasurableSpace α]
[MeasurableEq α]
:
instance
instMeasurableEqOfMeasurableSingletonClassOfCountable
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Countable α]
: