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 β.
We say that a filter f is measurably generated if every set s ∈ f includes a measurable
set t ∈ f. This property is useful, e.g., to extract a measurable witness of Filter.Eventually.
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
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 := ⋯ }
Instances For
theorem
MeasurableSpace.map_def
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{f : α → β}
{s : Set β}
:
MeasurableSet s ↔ MeasurableSet (f ⁻¹' s)
@[simp]
@[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
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.
Instances For
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 = MeasurableSpace.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.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.comap_mono
{α : Type u_1}
{β : Type u_2}
{m₁ m₂ : MeasurableSpace α}
{g : β → α}
(h : m₁ ≤ m₂)
:
MeasurableSpace.comap g m₁ ≤ MeasurableSpace.comap g m₂
@[simp]
@[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]
@[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 β)}
:
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.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.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_iff_comap_le
{α : Type u_1}
{β : Type u_2}
{m₁ : MeasurableSpace α}
{m₂ : MeasurableSpace β}
{f : α → β}
:
Measurable f ↔ MeasurableSpace.comap f m₂ ≤ m₁
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
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.mono
{α : Type u_1}
{β : Type u_2}
{ma ma' : MeasurableSpace α}
{mb mb' : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
(ha : ma ≤ ma')
(hb : mb' ≤ mb)
:
theorem
Measurable.iSup'
{α : Type u_1}
{β : Type u_2}
{ι : Sort uι}
{mα : ι → MeasurableSpace α}
{x✝ : MeasurableSpace β}
{f : α → β}
(i₀ : ι)
(h : Measurable f)
:
theorem
Measurable.sup_of_left
{α : Type u_1}
{β : Type u_2}
{mα mα' : MeasurableSpace α}
{x✝ : MeasurableSpace β}
{f : α → β}
(h : Measurable f)
:
theorem
Measurable.sup_of_right
{α : Type u_1}
{β : Type u_2}
{mα mα' : MeasurableSpace α}
{x✝ : MeasurableSpace β}
{f : α → β}
(h : Measurable f)
:
theorem
measurable_generateFrom
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
{s : Set (Set β)}
{f : α → β}
(h : ∀ t ∈ s, MeasurableSet (f ⁻¹' t))
:
theorem
Subsingleton.measurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[MeasurableSpace α]
[MeasurableSpace β]
[Subsingleton α]
:
theorem
measurable_of_subsingleton_codomain
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Subsingleton β]
(f : α → β)
:
theorem
measurable_one
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[One α]
:
theorem
measurable_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Zero α]
:
theorem
measurable_of_empty
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[IsEmpty α]
(f : α → β)
:
theorem
measurable_of_empty_codomain
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[IsEmpty β]
(f : α → β)
:
theorem
measurable_const'
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
(hf : ∀ (x y : β), f x = f y)
:
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 : α → β)
:
theorem
measurable_of_finite
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Finite α]
[MeasurableSingletonClass α]
(f : α → β)
:
theorem
Measurable.iterate
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
(hf : 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)
:
theorem
measurableSet_support
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Zero β]
[MeasurableSingletonClass β]
(hf : Measurable 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)
:
If a function coincides with a measurable function outside of a countable set, it is measurable.
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})
Equations
- ULift.instMeasurableSpace = MeasurableSpace.map ULift.up inst
@[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}
[MeasurableSpace α]
{f : α → ℕ}
:
(∀ (y : α), MeasurableSet (f ⁻¹' {f y})) → Measurable f
theorem
measurable_to_bool
{α : Type u_1}
[MeasurableSpace α]
{f : α → Bool}
(h : MeasurableSet (f ⁻¹' {true}))
:
theorem
measurable_to_prop
{α : Type u_1}
[MeasurableSpace α]
{f : α → Prop}
(h : MeasurableSet (f ⁻¹' {True}))
:
theorem
measurable_findGreatest'
{α : Type u_1}
[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}
[MeasurableSpace α]
{p : α → ℕ → Prop}
[(x : α) → DecidablePred (p x)]
{N : ℕ}
(hN : ∀ k ≤ N, MeasurableSet {x : α | p x k})
:
Measurable fun (x : α) => Nat.findGreatest (p x) N
theorem
measurable_find
{α : Type u_1}
[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 ⋯
instance
Quot.instMeasurableSpace
{α : Type u_6}
{r : α → α → Prop}
[m : MeasurableSpace α]
:
MeasurableSpace (Quot r)
Equations
- Quot.instMeasurableSpace = MeasurableSpace.map (Quot.mk r) m
Equations
- Quotient.instMeasurableSpace = MeasurableSpace.map Quotient.mk'' m
instance
QuotientGroup.measurableSpace
{G : Type u_6}
[Group G]
[MeasurableSpace G]
(S : Subgroup G)
:
MeasurableSpace (G ⧸ S)
Equations
- QuotientGroup.measurableSpace S = Quotient.instMeasurableSpace
instance
QuotientAddGroup.measurableSpace
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
(S : AddSubgroup G)
:
MeasurableSpace (G ⧸ S)
Equations
- QuotientAddGroup.measurableSpace S = Quotient.instMeasurableSpace
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_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}
:
Measurable QuotientGroup.mk
theorem
QuotientAddGroup.measurable_coe
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
{S : AddSubgroup G}
:
Measurable QuotientAddGroup.mk
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 ∘ QuotientGroup.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 ∘ QuotientAddGroup.mk)
instance
Quotient.instDiscreteMeasurableSpace
{α : Type u_6}
{s : Setoid α}
[MeasurableSpace α]
[DiscreteMeasurableSpace α]
:
Equations
- ⋯ = ⋯
instance
QuotientGroup.instDiscreteMeasurableSpace
{G : Type u_6}
[Group G]
[MeasurableSpace G]
[DiscreteMeasurableSpace G]
(S : Subgroup G)
:
DiscreteMeasurableSpace (G ⧸ S)
Equations
- ⋯ = ⋯
instance
QuotientAddGroup.instDiscreteMeasurableSpace
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
[DiscreteMeasurableSpace G]
(S : AddSubgroup G)
:
DiscreteMeasurableSpace (G ⧸ S)
Equations
- ⋯ = ⋯
Equations
- Subtype.instMeasurableSpace = MeasurableSpace.comap Subtype.val m
theorem
measurable_subtype_coe
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
:
Measurable Subtype.val
instance
Subtype.instMeasurableSingletonClass
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
[MeasurableSingletonClass α]
:
Equations
- ⋯ = ⋯
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.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 countaining 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
@[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 : β)
:
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
instance
Prod.instMeasurableSpace
{α : Type u_6}
{β : Type u_7}
[m₁ : MeasurableSpace α]
[m₂ : MeasurableSpace β]
:
MeasurableSpace (α × β)
Equations
- Prod.instMeasurableSpace = m₁.prod m₂
theorem
measurable_fst
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
:
Measurable Prod.fst
theorem
measurable_snd
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
:
Measurable Prod.snd
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.prod_mk
{α : 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.prod_map
{α : 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_prod_mk_left
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{x : α}
:
Measurable (Prod.mk x)
theorem
measurable_prod_mk_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_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 (α × β)
Equations
- ⋯ = ⋯
theorem
measurable_from_prod_countable'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable β]
{x✝ : MeasurableSpace γ}
{f : α × β → γ}
(hf : ∀ (y : β), Measurable fun (x : α) => f (x, y))
(h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y))
:
theorem
measurable_from_prod_countable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Countable β]
[MeasurableSingletonClass β]
{x✝ : MeasurableSpace γ}
{f : α × β → γ}
(hf : ∀ (y : β), Measurable fun (x : α) => f (x, y))
:
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 (α → β)].
instance
MeasurableSpace.pi
{δ : Type u_4}
{π : δ → Type u_6}
[m : (a : δ) → MeasurableSpace (π a)]
:
MeasurableSpace ((a : δ) → π a)
Equations
- MeasurableSpace.pi = ⨆ (a : δ), MeasurableSpace.comap (fun (b : (a : δ) → π a) => b a) (m a)
theorem
measurable_pi_iff
{α : Type u_1}
{δ : Type u_4}
{π : δ → Type u_6}
[MeasurableSpace α]
[(a : δ) → MeasurableSpace (π a)]
{g : α → (a : δ) → π a}
:
Measurable g ↔ ∀ (a : δ), Measurable fun (x : α) => g x a
theorem
measurable_pi_apply
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
(a : δ)
:
Measurable fun (f : (a : δ) → π a) => f a
theorem
Measurable.eval
{α : Type u_1}
{δ : Type u_4}
{π : δ → Type u_6}
[MeasurableSpace α]
[(a : δ) → MeasurableSpace (π a)]
{a : δ}
{g : α → (a : δ) → π a}
(hg : Measurable g)
:
Measurable fun (x : α) => g x a
theorem
measurable_pi_lambda
{α : Type u_1}
{δ : Type u_4}
{π : δ → Type u_6}
[MeasurableSpace α]
[(a : δ) → MeasurableSpace (π a)]
(f : α → (a : δ) → π a)
(hf : ∀ (a : δ), Measurable fun (c : α) => f c a)
:
theorem
measurable_update'
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{a : δ}
[DecidableEq δ]
:
Measurable fun (p : ((i : δ) → π i) × π a) => Function.update p.1 a p.2
The function (f, x) ↦ update f a x : (Π a, π a) × π a → Π a, π a is measurable.
theorem
measurable_uniqueElim
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
[Unique δ]
:
Measurable uniqueElim
theorem
measurable_updateFinset
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
[DecidableEq δ]
{s : Finset δ}
{x : (i : δ) → π i}
:
theorem
measurable_update
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
(f : (a : δ) → π a)
{a : δ}
[DecidableEq δ]
:
Measurable (Function.update f a)
The function update f a : π a → Π a, π 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}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{a : δ}
[DecidableEq δ]
{x : π a}
:
Measurable fun (x_1 : (a : δ) → π a) => Function.update x_1 a x
theorem
Set.measurable_restrict
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
(s : Set δ)
:
Measurable s.restrict
theorem
Set.measurable_restrict₂
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{s t : Set δ}
(hst : s ⊆ t)
:
Measurable (Set.restrict₂ hst)
theorem
Finset.measurable_restrict
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
(s : Finset δ)
:
Measurable s.restrict
theorem
Finset.measurable_restrict₂
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{s t : Finset δ}
(hst : s ⊆ t)
:
Measurable (Finset.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 (Set.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 : { x : α // x ∈ t } → γ}
(hf : Measurable f)
:
Measurable (Finset.restrict₂ hst f)
theorem
measurable_eq_mp
{δ : Type u_4}
(π : δ → Type u_6)
[(a : δ) → MeasurableSpace (π a)]
{i i' : δ}
(h : i = i')
:
Measurable ⋯.mp
theorem
Measurable.eq_mp
{δ : Type u_4}
(π : δ → Type u_6)
[(a : δ) → MeasurableSpace (π a)]
{β : Type u_7}
[MeasurableSpace β]
{i i' : δ}
(h : i = i')
{f : β → π i}
(hf : Measurable f)
:
Measurable fun (x : β) => ⋯.mp (f x)
theorem
measurable_piCongrLeft
{δ : Type u_4}
{δ' : Type u_5}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
(f : δ' ≃ δ)
:
Measurable ⇑(Equiv.piCongrLeft π f)
theorem
MeasurableSet.pi
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{s : Set δ}
{t : (i : δ) → Set (π i)}
(hs : s.Countable)
(ht : ∀ i ∈ s, MeasurableSet (t i))
:
MeasurableSet (s.pi t)
theorem
MeasurableSet.univ_pi
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
[Countable δ]
{t : (i : δ) → Set (π i)}
(ht : ∀ (i : δ), MeasurableSet (t i))
:
MeasurableSet (Set.univ.pi t)
theorem
measurableSet_pi_of_nonempty
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{s : Set δ}
{t : (i : δ) → Set (π i)}
(hs : s.Countable)
(h : (s.pi t).Nonempty)
:
MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)
theorem
measurableSet_pi
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{s : Set δ}
{t : (i : δ) → Set (π i)}
(hs : s.Countable)
:
MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
instance
Pi.instMeasurableSingletonClass
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
[Countable δ]
[∀ (a : δ), MeasurableSingletonClass (π a)]
:
MeasurableSingletonClass ((a : δ) → π a)
Equations
- ⋯ = ⋯
theorem
measurable_piEquivPiSubtypeProd_symm
{δ : Type u_4}
(π : δ → Type u_6)
[(a : δ) → MeasurableSpace (π a)]
(p : δ → Prop)
[DecidablePred p]
:
Measurable ⇑(Equiv.piEquivPiSubtypeProd p π).symm
theorem
measurable_piEquivPiSubtypeProd
{δ : Type u_4}
(π : δ → Type u_6)
[(a : δ) → MeasurableSpace (π a)]
(p : δ → Prop)
[DecidablePred p]
:
instance
TProd.instMeasurableSpace
{δ : Type u_4}
(π : δ → Type u_6)
[(x : δ) → MeasurableSpace (π x)]
(l : List δ)
:
MeasurableSpace (List.TProd π l)
Equations
- TProd.instMeasurableSpace π [] = PUnit.instMeasurableSpace
- TProd.instMeasurableSpace π (head :: is) = Prod.instMeasurableSpace
theorem
measurable_tProd_mk
{δ : Type u_4}
{π : δ → Type u_6}
[(x : δ) → MeasurableSpace (π x)]
(l : List δ)
:
theorem
measurable_tProd_elim
{δ : Type u_4}
{π : δ → Type u_6}
[(x : δ) → MeasurableSpace (π x)]
[DecidableEq δ]
{l : List δ}
{i : δ}
(hi : i ∈ l)
:
Measurable fun (v : List.TProd π l) => v.elim hi
theorem
measurable_tProd_elim'
{δ : Type u_4}
{π : δ → Type u_6}
[(x : δ) → MeasurableSpace (π x)]
[DecidableEq δ]
{l : List δ}
(h : ∀ (i : δ), i ∈ l)
:
theorem
MeasurableSet.tProd
{δ : Type u_4}
{π : δ → Type u_6}
[(x : δ) → MeasurableSpace (π x)]
(l : List δ)
{s : (i : δ) → Set (π i)}
(hs : ∀ (i : δ), MeasurableSet (s i))
:
MeasurableSet (Set.tprod l s)
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₂
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_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)
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)
@[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
This instance is useful when talking about Bernoulli sequences of random variables or binomial random graphs.
Equations
- ⋯ = ⋯
theorem
measurable_set_iff
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace β]
{g : β → Set α}
:
Measurable g ↔ ∀ (a : α), Measurable fun (x : β) => a ∈ g x
theorem
MeasurableSet.setOf_finite
{α : Type u_1}
[Countable α]
:
MeasurableSet {s : Set α | s.Finite}
theorem
MeasurableSet.setOf_infinite
{α : Type u_1}
[Countable α]
:
MeasurableSet {s : Set α | s.Infinite}
theorem
MeasurableSet.sep_finite
{α : Type u_1}
[Countable α]
{S : Set (Set α)}
(hS : MeasurableSet S)
:
MeasurableSet {s : Set α | s ∈ S ∧ s.Finite}
theorem
MeasurableSet.sep_infinite
{α : Type u_1}
[Countable α]
{S : Set (Set α)}
(hS : MeasurableSet S)
:
MeasurableSet {s : Set α | s ∈ S ∧ s.Infinite}
@[simp]
theorem
MeasurableSpace.generateFrom_singleton
{α : Type u_1}
(s : Set α)
:
MeasurableSpace.generateFrom {s} = MeasurableSpace.comap (fun (x : α) => x ∈ s) ⊤
The sigma-algebra generated by a single set s is {∅, s, sᶜ, univ}.
theorem
MeasurableSpace.generateFrom_singleton_le
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
(hs : MeasurableSet s)
:
A filter f is measurably generates if each s ∈ f includes a measurable t ∈ f.
- exists_measurable_subset : ∀ ⦃s : Set α⦄, s ∈ f → ∃ t ∈ f, MeasurableSet t ∧ t ⊆ s
Instances
instance
Filter.isMeasurablyGenerated_bot
{α : Type u_1}
[MeasurableSpace α]
:
⊥.IsMeasurablyGenerated
Equations
- ⋯ = ⋯
instance
Filter.isMeasurablyGenerated_top
{α : Type u_1}
[MeasurableSpace α]
:
⊤.IsMeasurablyGenerated
Equations
- ⋯ = ⋯
theorem
Filter.Eventually.exists_measurable_mem
{α : Type u_1}
[MeasurableSpace α]
{f : Filter α}
[f.IsMeasurablyGenerated]
{p : α → Prop}
(h : ∀ᶠ (x : α) in f, p x)
:
∃ s ∈ f, MeasurableSet s ∧ ∀ x ∈ s, p x
theorem
Filter.Eventually.exists_measurable_mem_of_smallSets
{α : Type u_1}
[MeasurableSpace α]
{f : Filter α}
[f.IsMeasurablyGenerated]
{p : Set α → Prop}
(h : ∀ᶠ (s : Set α) in f.smallSets, p s)
:
∃ s ∈ f, MeasurableSet s ∧ p s
instance
Filter.inf_isMeasurablyGenerated
{α : Type u_1}
[MeasurableSpace α]
(f g : Filter α)
[f.IsMeasurablyGenerated]
[g.IsMeasurablyGenerated]
:
(f ⊓ g).IsMeasurablyGenerated
Equations
- ⋯ = ⋯
theorem
Filter.principal_isMeasurablyGenerated_iff
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
:
(Filter.principal s).IsMeasurablyGenerated ↔ MeasurableSet s
theorem
MeasurableSet.principal_isMeasurablyGenerated
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
:
MeasurableSet s → (Filter.principal s).IsMeasurablyGenerated
Alias of the reverse direction of Filter.principal_isMeasurablyGenerated_iff.
instance
Filter.iInf_isMeasurablyGenerated
{α : Type u_1}
{ι : Sort uι}
[MeasurableSpace α]
{f : ι → Filter α}
[∀ (i : ι), (f i).IsMeasurablyGenerated]
:
(⨅ (i : ι), f i).IsMeasurablyGenerated
Equations
- ⋯ = ⋯
theorem
measurableSet_tendsto
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{x✝ : MeasurableSpace β}
[MeasurableSpace γ]
[Countable δ]
{l : Filter δ}
[l.IsCountablyGenerated]
(l' : Filter γ)
[l'.IsCountablyGenerated]
[hl' : l'.IsMeasurablyGenerated]
{f : δ → β → γ}
(hf : ∀ (i : δ), Measurable (f i))
:
MeasurableSet {x : β | Filter.Tendsto (fun (n : δ) => f n x) l l'}
The set of points for which a sequence of measurable functions converges to a given value is measurable.
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
Instances For
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.
theorem
MeasurableSet.iUnion_of_monotone_of_frequently
{α : Type u_1}
[MeasurableSpace α]
{ι : Type u_6}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hsm : Monotone s)
(hs : ∃ᶠ (i : ι) in Filter.atTop, MeasurableSet (s i))
:
MeasurableSet (⋃ (i : ι), s i)
theorem
MeasurableSet.iInter_of_antitone_of_frequently
{α : Type u_1}
[MeasurableSpace α]
{ι : Type u_6}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hsm : Antitone s)
(hs : ∃ᶠ (i : ι) in Filter.atTop, MeasurableSet (s i))
:
MeasurableSet (⋂ (i : ι), s i)
theorem
MeasurableSet.iUnion_of_monotone
{α : Type u_1}
[MeasurableSpace α]
{ι : Type u_6}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hsm : Monotone s)
(hs : ∀ (i : ι), MeasurableSet (s i))
:
MeasurableSet (⋃ (i : ι), s i)
theorem
MeasurableSet.iInter_of_antitone
{α : Type u_1}
[MeasurableSpace α]
{ι : Type u_6}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hsm : Antitone s)
(hs : ∀ (i : ι), MeasurableSet (s i))
:
MeasurableSet (⋂ (i : ι), s i)
Typeclasses on Subtype MeasurableSet #
instance
MeasurableSet.Subtype.instMembership
{α : Type u_1}
[MeasurableSpace α]
:
Membership α (Subtype MeasurableSet)
@[simp]
theorem
MeasurableSet.mem_coe
{α : Type u_1}
[MeasurableSpace α]
(a : α)
(s : Subtype MeasurableSet)
:
instance
MeasurableSet.Subtype.instEmptyCollection
{α : Type u_1}
[MeasurableSpace α]
:
EmptyCollection (Subtype MeasurableSet)
instance
MeasurableSet.Subtype.instInsert
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
:
@[simp]
theorem
MeasurableSet.coe_insert
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(a : α)
(s : Subtype MeasurableSet)
:
instance
MeasurableSet.Subtype.instSingleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
:
Equations
- MeasurableSet.Subtype.instSingleton = { singleton := fun (a : α) => ⟨{a}, ⋯⟩ }
@[simp]
theorem
MeasurableSet.coe_singleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(a : α)
:
↑{a} = {a}
instance
MeasurableSet.Subtype.instLawfulSingleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
:
LawfulSingleton α (Subtype MeasurableSet)
Equations
- ⋯ = ⋯
@[simp]
@[simp]
@[simp]
theorem
MeasurableSet.sup_eq_union
{α : Type u_1}
[MeasurableSpace α]
(s t : { s : Set α // MeasurableSet s })
:
@[simp]
@[simp]
theorem
MeasurableSet.inf_eq_inter
{α : Type u_1}
[MeasurableSpace α]
(s t : { s : Set α // MeasurableSet s })
:
@[simp]
@[simp]
Equations
- MeasurableSet.Subtype.instTop = { top := ⟨Set.univ, ⋯⟩ }
noncomputable instance
MeasurableSet.Subtype.instBooleanAlgebra
{α : Type u_1}
[MeasurableSpace α]
:
BooleanAlgebra (Subtype MeasurableSet)
Equations
- MeasurableSet.Subtype.instBooleanAlgebra = Function.Injective.booleanAlgebra (fun (a : Subtype MeasurableSet) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
MeasurableSet.measurableSet_blimsup
{α : Type u_1}
[MeasurableSpace α]
{s : ℕ → Set α}
{p : ℕ → Prop}
(h : ∀ (n : ℕ), p n → MeasurableSet (s n))
:
MeasurableSet (Filter.blimsup s Filter.atTop p)
theorem
MeasurableSet.measurableSet_bliminf
{α : Type u_1}
[MeasurableSpace α]
{s : ℕ → Set α}
{p : ℕ → Prop}
(h : ∀ (n : ℕ), p n → MeasurableSet (s n))
:
MeasurableSet (Filter.bliminf s Filter.atTop p)
theorem
MeasurableSet.measurableSet_limsup
{α : Type u_1}
[MeasurableSpace α]
{s : ℕ → Set α}
(hs : ∀ (n : ℕ), MeasurableSet (s n))
:
MeasurableSet (Filter.limsup s Filter.atTop)
theorem
MeasurableSet.measurableSet_liminf
{α : Type u_1}
[MeasurableSpace α]
{s : ℕ → Set α}
(hs : ∀ (n : ℕ), MeasurableSet (s n))
:
MeasurableSet (Filter.liminf s Filter.atTop)