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 β.
A measurable equivalence between measurable spaces is an equivalence which respects the σ-algebras, that is, for which both directions of the equivalence are measurable functions.
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.
Notation #
- We write
α ≃ᵐ βfor measurable equivalences between the measurable spacesαandβ. This should not be confused with≃ₘwhich is used for diffeomorphisms between manifolds.
Implementation notes #
Measurability of a function f : α → β between measurable spaces is
defined in terms of the Galois connection induced by f.
References #
Tags #
measurable space, σ-algebra, measurable function, measurable equivalence, 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 := ⋯ }
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.
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₁ : MeasurableSpace α}
{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₁ : MeasurableSpace α}
{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₁ : MeasurableSpace α}
{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₁ : MeasurableSpace α}
{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 : MeasurableSpace α}
{ma' : MeasurableSpace α}
{mb : MeasurableSpace β}
{mb' : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
(ha : ma ≤ ma')
(hb : mb' ≤ mb)
:
theorem
measurable_id''
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
(hm : m ≤ mα)
:
Measurable id
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_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Zero α]
:
theorem
measurable_one
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[One α]
:
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},
MeasurableSet s → Measurable f → Measurable g → Measurable (Set.piecewise s f g)
theorem
Measurable.ite
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{g : α → β}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
{p : α → Prop}
:
∀ {x : DecidablePred p},
MeasurableSet {a : α | p a} → Measurable f → Measurable g → Measurable fun (x_1 : α) => if p x_1 then f x_1 else g x_1
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 (Set.indicator s f)
theorem
measurable_indicator_const_iff
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Zero β]
[MeasurableSingletonClass β]
(b : β)
[NeZero b]
:
Measurable (Set.indicator s 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_support
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[Zero β]
[MeasurableSingletonClass β]
(hf : Measurable f)
:
theorem
measurableSet_mulSupport
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[One β]
[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 : Set.Countable {x : α | f x ≠ g x})
:
If a function coincides with a measurable function outside of a countable set, it is measurable.
Equations
Equations
Equations
instance
Subsingleton.measurableSingletonClass
{α : Type u_6}
[MeasurableSpace α]
[Subsingleton α]
:
Equations
- ⋯ = ⋯
Equations
Equations
- ⋯ = ⋯
Equations
Equations
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}))
:
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
QuotientAddGroup.measurableSpace
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
(S : AddSubgroup G)
:
MeasurableSpace (G ⧸ S)
Equations
- QuotientAddGroup.measurableSpace S = Quotient.instMeasurableSpace
instance
QuotientGroup.measurableSpace
{G : Type u_6}
[Group G]
[MeasurableSpace G]
(S : Subgroup G)
:
MeasurableSpace (G ⧸ S)
Equations
- QuotientGroup.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
QuotientAddGroup.measurable_coe
{G : Type u_6}
[AddGroup G]
[MeasurableSpace G]
{S : AddSubgroup G}
:
Measurable QuotientAddGroup.mk
theorem
QuotientGroup.measurable_coe
{G : Type u_6}
[Group G]
[MeasurableSpace G]
{S : Subgroup G}
:
Measurable 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)
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)
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 : α) => { val := f x, property := ⋯ }
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
measurable_inclusion
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{t : Set α}
(h : s ⊆ t)
:
theorem
MeasurableSet.image_inclusion'
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{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 : Set α}
{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 : Set α}
{t : Set α}
{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 : Set α)
(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 (Set.restrict s f))
(h₂ : Measurable (Set.restrict sᶜ 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 { val := x, property := hx } else g { val := x, property := hx }
theorem
measurable_of_measurable_on_compl_finite
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSingletonClass α]
{f : α → β}
(s : Set α)
(hs : Set.Finite s)
(hf : Measurable (Set.restrict sᶜ f))
:
theorem
measurable_of_measurable_on_compl_singleton
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSingletonClass α]
{f : α → β}
(a : α)
(hf : Measurable (Set.restrict {x : α | x ≠ a} f))
:
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
- MeasurableSpace.prod m₁ m₂ = MeasurableSpace.comap Prod.fst m₁ ⊔ MeasurableSpace.comap Prod.snd m₂
instance
Prod.instMeasurableSpace
{α : Type u_6}
{β : Type u_7}
[m₁ : MeasurableSpace α]
[m₂ : MeasurableSpace β]
:
MeasurableSpace (α × β)
Equations
- Prod.instMeasurableSpace = MeasurableSpace.prod m₁ m₂
theorem
measurable_fst
{α : Type u_1}
{β : Type u_2}
:
∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst
theorem
measurable_snd
{α : Type u_1}
{β : Type u_2}
:
∀ {x : MeasurableSpace α} {x_1 : 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_1 : MeasurableSpace γ} {f : α → β} {g : α → γ},
Measurable f → 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 : Set.Nonempty (s ×ˢ t))
:
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 β]
[MeasurableSingletonClass β]
:
∀ {x : MeasurableSpace γ} {f : α × β → γ}, (∀ (y : β), Measurable fun (x : α) => f (x, y)) → Measurable f
theorem
Measurable.find
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
:
∀ {x : MeasurableSpace α} {f : ℕ → α → β} {p : ℕ → α → Prop} [inst : (n : ℕ) → DecidablePred (p n)],
(∀ (n : ℕ), Measurable (f n)) →
(∀ (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 { val := x, property := hxi } = f j { val := x, property := 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 { val := x, property := hxi } = f j { val := x, property := 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 (α → β)].
@[deprecated exists_measurable_piecewise]
theorem
exists_measurable_piecewise_nat
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{m : MeasurableSpace α}
(t : ℕ → Set β)
(t_meas : ∀ (n : ℕ), MeasurableSet (t n))
(t_disj : Pairwise (Disjoint on t))
(g : ℕ → β → α)
(hg : ∀ (n : ℕ), Measurable (g n))
:
∃ (f : β → α), Measurable f ∧ ∀ (n : ℕ), ∀ x ∈ t n, f x = g n x
Given countably many disjoint measurable sets t n and countably many measurable
functions g n, one can construct a measurable function that coincides with g n on t n.
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}
[Unique δ]
[(i : δ) → MeasurableSpace (π i)]
:
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
measurable_eq_mp
{δ : Type u_4}
(π : δ → Type u_6)
[(a : δ) → MeasurableSpace (π a)]
{i : δ}
{i' : δ}
(h : i = i')
:
Measurable (Eq.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 : β) => Eq.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 : Set.Countable s)
(ht : ∀ i ∈ s, MeasurableSet (t i))
:
MeasurableSet (Set.pi s 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.pi Set.univ t)
theorem
measurableSet_pi_of_nonempty
{δ : Type u_4}
{π : δ → Type u_6}
[(a : δ) → MeasurableSpace (π a)]
{s : Set δ}
{t : (i : δ) → Set (π i)}
(hs : Set.Countable s)
(h : Set.Nonempty (Set.pi s t))
:
MeasurableSet (Set.pi s 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 : Set.Countable s)
:
MeasurableSet (Set.pi s t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ Set.pi s 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) => List.TProd.elim v 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 : α ⊕ β → γ}, Measurable (f ∘ Sum.inl) → Measurable (f ∘ Sum.inr) → Measurable f
theorem
Measurable.sumElim
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{mβ : MeasurableSpace β}
:
∀ {x : MeasurableSpace γ} {f : α → γ} {g : β → γ}, Measurable f → 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_1 : MeasurableSpace δ} {f : α → β} {g : γ → δ},
Measurable f → 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 : α → Prop}
{q : α → Prop}
(hp : Measurable p)
(hq : Measurable q)
:
Measurable fun (a : α) => p a ∧ q a
theorem
Measurable.or
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
{q : α → Prop}
(hp : Measurable p)
(hq : Measurable q)
:
Measurable fun (a : α) => p a ∨ q a
theorem
Measurable.imp
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
{q : α → Prop}
(hp : Measurable p)
(hq : Measurable q)
:
Measurable fun (a : α) => p a → q a
theorem
Measurable.iff
{α : Type u_1}
[MeasurableSpace α]
{p : α → Prop}
{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
@[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}.
structure
MeasurableEmbedding
{α : Type u_6}
{β : Type u_7}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
:
A map f : α → β is called a measurable embedding if it is injective, measurable, and sends
measurable sets to measurable sets. The latter assumption can be replaced with “f has measurable
inverse g : Set.range f → α”, see MeasurableEmbedding.measurable_rangeSplitting,
MeasurableEmbedding.of_measurable_inverse_range, and
MeasurableEmbedding.of_measurable_inverse.
One more interpretation: f is a measurable embedding if it defines a measurable equivalence to its
range and the range is a measurable set. One implication is formalized as
MeasurableEmbedding.equivRange; the other one follows from
MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.subtype_coe, and
MeasurableEmbedding.comp.
- injective : Function.Injective f
A measurable embedding is injective.
- measurable : Measurable f
A measurable embedding is a measurable function.
- measurableSet_image' : ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)
The image of a measurable set under a measurable embedding is a measurable set.
theorem
MeasurableEmbedding.measurableSet_image
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
{s : Set α}
:
MeasurableSet (f '' s) ↔ MeasurableSet s
theorem
MeasurableEmbedding.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : α → β}
{g : β → γ}
(hg : MeasurableEmbedding g)
(hf : MeasurableEmbedding f)
:
MeasurableEmbedding (g ∘ f)
theorem
MeasurableEmbedding.subtype_coe
{α : Type u_1}
{mα : MeasurableSpace α}
{s : Set α}
(hs : MeasurableSet s)
:
MeasurableEmbedding Subtype.val
theorem
MeasurableEmbedding.measurableSet_range
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEmbedding.measurableSet_preimage
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
{s : Set β}
:
MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)
theorem
MeasurableEmbedding.measurable_rangeSplitting
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
:
theorem
MeasurableEmbedding.measurable_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : α → β}
(hf : MeasurableEmbedding f)
{g : α → γ}
{g' : β → γ}
(hg : Measurable g)
(hg' : Measurable g')
:
Measurable (Function.extend f g g')
theorem
MeasurableEmbedding.exists_measurable_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : α → β}
(hf : MeasurableEmbedding f)
{g : α → γ}
(hg : Measurable g)
(hne : β → Nonempty γ)
:
∃ (g' : β → γ), Measurable g' ∧ g' ∘ f = g
theorem
MeasurableEmbedding.measurable_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : α → β}
{g : β → γ}
(hg : MeasurableEmbedding g)
:
Measurable (g ∘ f) ↔ Measurable f
theorem
MeasurableSet.exists_measurable_proj
{α : Type u_1}
:
∀ {x : MeasurableSpace α} {s : Set α},
MeasurableSet s → Set.Nonempty s → ∃ (f : α → ↑s), Measurable f ∧ ∀ (x : ↑s), f ↑x = x
structure
MeasurableEquiv
(α : Type u_6)
(β : Type u_7)
[MeasurableSpace α]
[MeasurableSpace β]
extends
Equiv
:
Type (max u_6 u_7)
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- measurable_toFun : Measurable ⇑self.toEquiv
The forward function of a measurable equivalence is measurable.
- measurable_invFun : Measurable ⇑self.symm
The inverse function of a measurable equivalence is measurable.
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
Equations
- «term_≃ᵐ_» = Lean.ParserDescr.trailingNode `term_≃ᵐ_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵐ ") (Lean.ParserDescr.cat `term 26))
theorem
MeasurableEquiv.toEquiv_injective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
Function.Injective MeasurableEquiv.toEquiv
instance
MeasurableEquiv.instEquivLike
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
@[simp]
theorem
MeasurableEquiv.coe_toEquiv
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
⇑e.toEquiv = ⇑e
theorem
MeasurableEquiv.measurable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
Measurable ⇑e
@[simp]
theorem
MeasurableEquiv.coe_mk
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ β)
(h1 : Measurable ⇑e)
(h2 : Measurable ⇑e.symm)
:
⇑{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 } = ⇑e
Any measurable space is equivalent to itself.
Equations
- MeasurableEquiv.refl α = { toEquiv := Equiv.refl α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Equations
- MeasurableEquiv.instInhabited = { default := MeasurableEquiv.refl α }
def
MeasurableEquiv.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
:
α ≃ᵐ γ
The composition of equivalences between measurable spaces.
Equations
- ab.trans bc = { toEquiv := ab.trans bc.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
theorem
MeasurableEquiv.coe_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
:
def
MeasurableEquiv.symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(ab : α ≃ᵐ β)
:
β ≃ᵐ α
The inverse of an equivalence between measurable spaces.
Equations
- ab.symm = { toEquiv := ab.symm, measurable_toFun := ⋯, measurable_invFun := ⋯ }
@[simp]
theorem
MeasurableEquiv.coe_toEquiv_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
⇑e.symm = ⇑e.symm
def
MeasurableEquiv.Simps.apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(h : α ≃ᵐ β)
:
α → β
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
MeasurableEquiv.Simps.symm_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(h : α ≃ᵐ β)
:
β → α
See Note [custom simps projection]
Equations
- MeasurableEquiv.Simps.symm_apply h = ⇑h.symm
theorem
MeasurableEquiv.ext
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{e₁ : α ≃ᵐ β}
{e₂ : α ≃ᵐ β}
(h : ⇑e₁ = ⇑e₂)
:
e₁ = e₂
@[simp]
theorem
MeasurableEquiv.symm_mk
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ β)
(h1 : Measurable ⇑e)
(h2 : Measurable ⇑e.symm)
:
{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm = { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }
@[simp]
theorem
MeasurableEquiv.trans_toEquiv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
:
(ab.trans bc).toEquiv = ab.trans bc.toEquiv
@[simp]
theorem
MeasurableEquiv.refl_apply
(α : Type u_6)
[MeasurableSpace α]
(a : α)
:
(MeasurableEquiv.refl α) a = a
@[simp]
theorem
MeasurableEquiv.trans_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
:
∀ (a : α), (ab.trans bc) a = bc (ab a)
@[simp]
theorem
MeasurableEquiv.refl_toEquiv
(α : Type u_6)
[MeasurableSpace α]
:
(MeasurableEquiv.refl α).toEquiv = Equiv.refl α
@[simp]
theorem
MeasurableEquiv.symm_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
e.symm.symm = e
theorem
MeasurableEquiv.symm_bijective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
Function.Bijective MeasurableEquiv.symm
@[simp]
theorem
MeasurableEquiv.symm_refl
(α : Type u_6)
[MeasurableSpace α]
:
(MeasurableEquiv.refl α).symm = MeasurableEquiv.refl α
@[simp]
theorem
MeasurableEquiv.symm_comp_self
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
@[simp]
theorem
MeasurableEquiv.self_comp_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
@[simp]
theorem
MeasurableEquiv.apply_symm_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(y : β)
:
e (e.symm y) = y
@[simp]
theorem
MeasurableEquiv.symm_apply_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(x : α)
:
e.symm (e x) = x
@[simp]
theorem
MeasurableEquiv.symm_trans_self
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
e.symm.trans e = MeasurableEquiv.refl β
@[simp]
theorem
MeasurableEquiv.self_trans_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
e.trans e.symm = MeasurableEquiv.refl α
theorem
MeasurableEquiv.surjective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.bijective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.injective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
@[simp]
theorem
MeasurableEquiv.symm_preimage_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set β)
:
theorem
MeasurableEquiv.image_eq_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set α)
:
theorem
MeasurableEquiv.preimage_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set α)
:
theorem
MeasurableEquiv.image_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set β)
:
theorem
MeasurableEquiv.eq_image_iff_symm_image_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set β)
(t : Set α)
:
@[simp]
theorem
MeasurableEquiv.image_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set β)
:
@[simp]
theorem
MeasurableEquiv.preimage_image
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set α)
:
@[simp]
theorem
MeasurableEquiv.measurableSet_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
{s : Set β}
:
MeasurableSet (⇑e ⁻¹' s) ↔ MeasurableSet s
@[simp]
theorem
MeasurableEquiv.measurableSet_image
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
{s : Set α}
:
MeasurableSet (⇑e '' s) ↔ MeasurableSet s
@[simp]
theorem
MeasurableEquiv.map_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
MeasurableSpace.map (⇑e) inst✝¹ = inst✝
theorem
MeasurableEquiv.measurableEmbedding
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
A measurable equivalence is a measurable embedding.
def
MeasurableEquiv.cast
{α : Type u_6}
{β : Type u_6}
[i₁ : MeasurableSpace α]
[i₂ : MeasurableSpace β]
(h : α = β)
(hi : HEq i₁ i₂)
:
α ≃ᵐ β
Equal measurable spaces are equivalent.
Equations
- MeasurableEquiv.cast h hi = { toEquiv := Equiv.cast h, measurable_toFun := ⋯, measurable_invFun := ⋯ }
theorem
MeasurableEquiv.measurable_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{f : β → γ}
(e : α ≃ᵐ β)
:
Measurable (f ∘ ⇑e) ↔ Measurable f
def
MeasurableEquiv.ofUniqueOfUnique
(α : Type u_6)
(β : Type u_7)
[MeasurableSpace α]
[MeasurableSpace β]
[Unique α]
[Unique β]
:
α ≃ᵐ β
Any two types with unique elements are measurably equivalent.
Equations
- MeasurableEquiv.ofUniqueOfUnique α β = { toEquiv := Equiv.equivOfUnique α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.prodCongr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
(ab : α ≃ᵐ β)
(cd : γ ≃ᵐ δ)
:
Products of equivalent measurable spaces are equivalent.
Equations
- MeasurableEquiv.prodCongr ab cd = { toEquiv := Equiv.prodCongr ab.toEquiv cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.prodComm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
Products of measurable spaces are symmetric.
Equations
- MeasurableEquiv.prodComm = { toEquiv := Equiv.prodComm α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.prodAssoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
:
Products of measurable spaces are associative.
Equations
- MeasurableEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.sumCongr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
(ab : α ≃ᵐ β)
(cd : γ ≃ᵐ δ)
:
Sums of measurable spaces are symmetric.
Equations
- MeasurableEquiv.sumCongr ab cd = { toEquiv := Equiv.sumCongr ab.toEquiv cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.Set.prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(s : Set α)
(t : Set β)
:
s ×ˢ t ≃ (s × t) as measurable spaces.
Equations
- MeasurableEquiv.Set.prod s t = { toEquiv := Equiv.Set.prod s t, measurable_toFun := ⋯, measurable_invFun := ⋯ }
univ α ≃ α as measurable spaces.
Equations
- MeasurableEquiv.Set.univ α = { toEquiv := Equiv.Set.univ α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
{a} ≃ Unit as measurable spaces.
Equations
- MeasurableEquiv.Set.singleton a = { toEquiv := Equiv.Set.singleton a, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.Set.rangeInl
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
α is equivalent to its image in α ⊕ β as measurable spaces.
Equations
- MeasurableEquiv.Set.rangeInl = { toEquiv := Equiv.Set.rangeInl α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.Set.rangeInr
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
β is equivalent to its image in α ⊕ β as measurable spaces.
Equations
- MeasurableEquiv.Set.rangeInr = { toEquiv := Equiv.Set.rangeInr α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.sumProdDistrib
(α : Type u_6)
(β : Type u_7)
(γ : Type u_8)
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
:
Products distribute over sums (on the right) as measurable spaces.
Equations
- MeasurableEquiv.sumProdDistrib α β γ = { toEquiv := Equiv.sumProdDistrib α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.prodSumDistrib
(α : Type u_6)
(β : Type u_7)
(γ : Type u_8)
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
:
Products distribute over sums (on the left) as measurable spaces.
Equations
- One or more equations did not get rendered due to their size.
def
MeasurableEquiv.sumProdSum
(α : Type u_6)
(β : Type u_7)
(γ : Type u_8)
(δ : Type u_9)
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
:
Products distribute over sums as measurable spaces.
Equations
- MeasurableEquiv.sumProdSum α β γ δ = (MeasurableEquiv.sumProdDistrib α β (γ ⊕ δ)).trans (MeasurableEquiv.sumCongr (MeasurableEquiv.prodSumDistrib α γ δ) (MeasurableEquiv.prodSumDistrib β γ δ))
def
MeasurableEquiv.piCongrRight
{δ' : Type u_5}
{π : δ' → Type u_6}
{π' : δ' → Type u_7}
[(x : δ') → MeasurableSpace (π x)]
[(x : δ') → MeasurableSpace (π' x)]
(e : (a : δ') → π a ≃ᵐ π' a)
:
((a : δ') → π a) ≃ᵐ ((a : δ') → π' a)
A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence
between Π a, β₁ a and Π a, β₂ a.
Equations
- MeasurableEquiv.piCongrRight e = { toEquiv := Equiv.piCongrRight fun (a : δ') => (e a).toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.piCongrLeft
{δ : Type u_4}
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
(f : δ ≃ δ')
:
((b : δ) → π (f b)) ≃ᵐ ((a : δ') → π a)
Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.
Equations
- MeasurableEquiv.piCongrLeft π f = let __src := Equiv.piCongrLeft π f; { toEquiv := __src, measurable_toFun := ⋯, measurable_invFun := ⋯ }
theorem
MeasurableEquiv.coe_piCongrLeft
{δ : Type u_4}
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
(f : δ ≃ δ')
:
⇑(MeasurableEquiv.piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)
@[simp]
theorem
MeasurableEquiv.piMeasurableEquivTProd_symm_apply
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
[DecidableEq δ']
{l : List δ'}
(hnd : List.Nodup l)
(h : ∀ (i : δ'), i ∈ l)
:
⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h).symm = List.TProd.elim' h
@[simp]
theorem
MeasurableEquiv.piMeasurableEquivTProd_apply
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
[DecidableEq δ']
{l : List δ'}
(hnd : List.Nodup l)
(h : ∀ (i : δ'), i ∈ l)
:
⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h) = List.TProd.mk l
def
MeasurableEquiv.piMeasurableEquivTProd
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
[DecidableEq δ']
{l : List δ'}
(hnd : List.Nodup l)
(h : ∀ (i : δ'), i ∈ l)
:
((i : δ') → π i) ≃ᵐ List.TProd π l
Pi-types are measurably equivalent to iterated products.
Equations
- MeasurableEquiv.piMeasurableEquivTProd hnd h = { toEquiv := List.TProd.piEquivTProd hnd h, measurable_toFun := ⋯, measurable_invFun := ⋯ }
@[simp]
theorem
MeasurableEquiv.piUnique_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[Unique δ']
:
⇑(MeasurableEquiv.piUnique π) = fun (f : (i : δ') → π i) => f default
@[simp]
theorem
MeasurableEquiv.piUnique_symm_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[Unique δ']
:
⇑(MeasurableEquiv.piUnique π).symm = uniqueElim
def
MeasurableEquiv.piUnique
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[Unique δ']
:
((i : δ') → π i) ≃ᵐ π default
The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆ when the domain of π only contains ⋆
Equations
- MeasurableEquiv.piUnique π = { toEquiv := Equiv.piUnique π, measurable_toFun := ⋯, measurable_invFun := ⋯ }
@[simp]
theorem
MeasurableEquiv.funUnique_symm_apply
(α : Type u_8)
(β : Type u_9)
[Unique α]
[MeasurableSpace β]
:
⇑(MeasurableEquiv.funUnique α β).symm = uniqueElim
@[simp]
theorem
MeasurableEquiv.funUnique_apply
(α : Type u_8)
(β : Type u_9)
[Unique α]
[MeasurableSpace β]
:
⇑(MeasurableEquiv.funUnique α β) = fun (f : α → β) => f default
def
MeasurableEquiv.funUnique
(α : Type u_8)
(β : Type u_9)
[Unique α]
[MeasurableSpace β]
:
(α → β) ≃ᵐ β
If α has a unique term, then the type of function α → β is measurably equivalent to β.
Equations
- MeasurableEquiv.funUnique α β = MeasurableEquiv.piUnique fun (a : α) => β
@[simp]
theorem
MeasurableEquiv.piFinTwo_apply
(α : Fin 2 → Type u_8)
[(i : Fin 2) → MeasurableSpace (α i)]
:
⇑(MeasurableEquiv.piFinTwo α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)
@[simp]
theorem
MeasurableEquiv.piFinTwo_symm_apply
(α : Fin 2 → Type u_8)
[(i : Fin 2) → MeasurableSpace (α i)]
:
⇑(MeasurableEquiv.piFinTwo α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
The space Π i : Fin 2, α i is measurably equivalent to α 0 × α 1.
Equations
- MeasurableEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
@[simp]
@[simp]
The space Fin 2 → α is measurably equivalent to α × α.
Equations
- MeasurableEquiv.finTwoArrow = MeasurableEquiv.piFinTwo fun (x : Fin 2) => α
@[simp]
theorem
MeasurableEquiv.piFinSuccAbove_symm_apply
{n : ℕ}
(α : Fin (n + 1) → Type u_8)
[(i : Fin (n + 1)) → MeasurableSpace (α i)]
(i : Fin (n + 1))
:
⇑(MeasurableEquiv.piFinSuccAbove α i).symm = fun (f : α i × ((j : Fin n) → α (Fin.succAbove i j))) =>
Fin.insertNth i f.1 f.2
@[simp]
theorem
MeasurableEquiv.piFinSuccAbove_apply
{n : ℕ}
(α : Fin (n + 1) → Type u_8)
[(i : Fin (n + 1)) → MeasurableSpace (α i)]
(i : Fin (n + 1))
:
⇑(MeasurableEquiv.piFinSuccAbove α i) = fun (f : (j : Fin (n + 1)) → α j) =>
(f i, fun (j : Fin n) => f (Fin.succAbove i j))
def
MeasurableEquiv.piFinSuccAbove
{n : ℕ}
(α : Fin (n + 1) → Type u_8)
[(i : Fin (n + 1)) → MeasurableSpace (α i)]
(i : Fin (n + 1))
:
Measurable equivalence between Π j : Fin (n + 1), α j and
α i × Π j : Fin n, α (Fin.succAbove i j).
Equations
- MeasurableEquiv.piFinSuccAbove α i = { toEquiv := Equiv.piFinSuccAbove α i, measurable_toFun := ⋯, measurable_invFun := ⋯ }
@[simp]
theorem
MeasurableEquiv.piEquivPiSubtypeProd_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
(p : δ' → Prop)
[DecidablePred p]
:
⇑(MeasurableEquiv.piEquivPiSubtypeProd π p) = fun (f : (i : δ') → π i) =>
(fun (x : { x : δ' // p x }) => f ↑x, fun (x : { x : δ' // ¬p x }) => f ↑x)
@[simp]
theorem
MeasurableEquiv.piEquivPiSubtypeProd_symm_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
(p : δ' → Prop)
[DecidablePred p]
:
⇑(MeasurableEquiv.piEquivPiSubtypeProd π p).symm = fun (f : ((i : { x : δ' // p x }) → π ↑i) × ((i : { x : δ' // ¬p x }) → π ↑i)) (x : δ') =>
if h : p x then f.1 { val := x, property := h } else f.2 { val := x, property := h }
def
MeasurableEquiv.piEquivPiSubtypeProd
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
(p : δ' → Prop)
[DecidablePred p]
:
Measurable equivalence between (dependent) functions on a type and pairs of functions on
{i // p i} and {i // ¬p i}. See also Equiv.piEquivPiSubtypeProd.
Equations
- MeasurableEquiv.piEquivPiSubtypeProd π p = { toEquiv := Equiv.piEquivPiSubtypeProd p π, measurable_toFun := ⋯, measurable_invFun := ⋯ }
def
MeasurableEquiv.sumPiEquivProdPi
{δ : Type u_4}
{δ' : Type u_5}
(α : δ ⊕ δ' → Type u_8)
[(i : δ ⊕ δ') → MeasurableSpace (α i)]
:
The measurable equivalence between the pi type over a sum type and a product of pi-types.
This is similar to MeasurableEquiv.piEquivPiSubtypeProd.
Equations
- MeasurableEquiv.sumPiEquivProdPi α = let __src := Equiv.sumPiEquivProdPi α; { toEquiv := __src, measurable_toFun := ⋯, measurable_invFun := ⋯ }
theorem
MeasurableEquiv.coe_sumPiEquivProdPi
{δ : Type u_4}
{δ' : Type u_5}
(α : δ ⊕ δ' → Type u_8)
[(i : δ ⊕ δ') → MeasurableSpace (α i)]
:
theorem
MeasurableEquiv.coe_sumPiEquivProdPi_symm
{δ : Type u_4}
{δ' : Type u_5}
(α : δ ⊕ δ' → Type u_8)
[(i : δ ⊕ δ') → MeasurableSpace (α i)]
:
⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm
def
MeasurableEquiv.piFinsetUnion
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[DecidableEq δ']
{s : Finset δ'}
{t : Finset δ'}
(h : Disjoint s t)
:
The measurable equivalence (∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i)
for disjoint finsets s and t. Equiv.piFinsetUnion as a measurable equivalence.
Equations
- One or more equations did not get rendered due to their size.
def
MeasurableEquiv.sumCompl
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
If s is a measurable set in a measurable space, that space is equivalent
to the sum of s and sᶜ.
Equations
- MeasurableEquiv.sumCompl hs = { toEquiv := Equiv.sumCompl fun (x : α) => x ∈ s, measurable_toFun := ⋯, measurable_invFun := ⋯ }
@[simp]
theorem
MeasurableEquiv.ofInvolutive_toEquiv
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(hf : Function.Involutive f)
(hf' : Measurable f)
:
(MeasurableEquiv.ofInvolutive f hf hf').toEquiv = Function.Involutive.toPerm f hf
def
MeasurableEquiv.ofInvolutive
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(hf : Function.Involutive f)
(hf' : Measurable f)
:
α ≃ᵐ α
Convert a measurable involutive function f to a measurable permutation with
toFun = invFun = f. See also Function.Involutive.toPerm.
Equations
- MeasurableEquiv.ofInvolutive f hf hf' = { toEquiv := Function.Involutive.toPerm f hf, measurable_toFun := hf', measurable_invFun := hf' }
@[simp]
theorem
MeasurableEquiv.ofInvolutive_apply
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(hf : Function.Involutive f)
(hf' : Measurable f)
(a : α)
:
(MeasurableEquiv.ofInvolutive f hf hf') a = f a
@[simp]
theorem
MeasurableEquiv.ofInvolutive_symm
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(hf : Function.Involutive f)
(hf' : Measurable f)
:
(MeasurableEquiv.ofInvolutive f hf hf').symm = MeasurableEquiv.ofInvolutive f hf hf'
@[simp]
theorem
MeasurableEmbedding.comap_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
:
MeasurableSpace.comap f inst✝ = inst✝¹
theorem
MeasurableEmbedding.iff_comap_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
:
MeasurableEmbedding f ↔ Function.Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (Set.range f)
noncomputable def
MeasurableEmbedding.equivImage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(s : Set α)
(hf : MeasurableEmbedding f)
:
A set is equivalent to its image under a function f as measurable spaces,
if f is a measurable embedding
Equations
- MeasurableEmbedding.equivImage s hf = { toEquiv := Equiv.Set.image f s ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
noncomputable def
MeasurableEmbedding.equivRange
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
:
The domain of f is equivalent to its range as measurable spaces,
if f is a measurable embedding
Equations
- MeasurableEmbedding.equivRange hf = (MeasurableEquiv.Set.univ α).symm.trans ((MeasurableEmbedding.equivImage Set.univ hf).trans (MeasurableEquiv.cast ⋯ ⋯))
theorem
MeasurableEmbedding.of_measurable_inverse_on_range
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{g : ↑(Set.range f) → α}
(hf₁ : Measurable f)
(hf₂ : MeasurableSet (Set.range f))
(hg : Measurable g)
(H : Function.LeftInverse g (Set.rangeFactorization f))
:
theorem
MeasurableEmbedding.of_measurable_inverse
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{g : β → α}
(hf₁ : Measurable f)
(hf₂ : MeasurableSet (Set.range f))
(hg : Measurable g)
(H : Function.LeftInverse g f)
:
noncomputable def
MeasurableEmbedding.schroederBernstein
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{g : β → α}
(hf : MeasurableEmbedding f)
(hg : MeasurableEmbedding g)
:
α ≃ᵐ β
The measurable Schröder-Bernstein Theorem: given measurable embeddings
α → β and β → α, we can find a measurable equivalence α ≃ᵐ β.
Equations
- One or more equations did not get rendered due to their size.
theorem
MeasurableSpace.comap_compl
{α : Type u_1}
{β : Type u_2}
{m' : MeasurableSpace β}
[BooleanAlgebra β]
(h : Measurable compl)
(f : α → β)
:
MeasurableSpace.comap (fun (a : α) => (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance
@[simp]
theorem
MeasurableSpace.comap_not
{α : Type u_1}
(p : α → Prop)
:
MeasurableSpace.comap (fun (a : α) => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance
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
- Filter.iInf_isMeasurablyGenerated
- Filter.inf_isMeasurablyGenerated
- Filter.isMeasurablyGenerated_bot
- Filter.isMeasurablyGenerated_top
- MeasureTheory.ae_isMeasurablyGenerated
- atBot_isMeasurablyGenerated
- atTop_isMeasurablyGenerated
- instIsMeasurablyGeneratedCocompact
- nhdsWithin_Icc_isMeasurablyGenerated
- nhdsWithin_Ici_isMeasurablyGenerated
- nhdsWithin_Iic_isMeasurablyGenerated
- nhdsWithin_Iio_isMeasurablyGenerated
- nhdsWithin_Ioi_isMeasurablyGenerated
- nhdsWithin_uIcc_isMeasurablyGenerated
- nhds_isMeasurablyGenerated
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
theorem
Filter.Eventually.exists_measurable_mem
{α : Type u_1}
[MeasurableSpace α]
{f : Filter α}
[Filter.IsMeasurablyGenerated f]
{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 α}
[Filter.IsMeasurablyGenerated f]
{p : Set α → Prop}
(h : ∀ᶠ (s : Set α) in Filter.smallSets f, p s)
:
∃ s ∈ f, MeasurableSet s ∧ p s
instance
Filter.inf_isMeasurablyGenerated
{α : Type u_1}
[MeasurableSpace α]
(f : Filter α)
(g : Filter α)
[Filter.IsMeasurablyGenerated f]
[Filter.IsMeasurablyGenerated g]
:
Equations
- ⋯ = ⋯
theorem
MeasurableSet.principal_isMeasurablyGenerated
{α : Type u_1}
[MeasurableSpace α]
{s : Set α}
:
Alias of the reverse direction of Filter.principal_isMeasurablyGenerated_iff.
instance
Filter.iInf_isMeasurablyGenerated
{α : Type u_1}
{ι : Sort uι}
[MeasurableSpace α]
{f : ι → Filter α}
[∀ (i : ι), Filter.IsMeasurablyGenerated (f i)]
:
Filter.IsMeasurablyGenerated (⨅ (i : ι), f i)
Equations
- ⋯ = ⋯
theorem
measurableSet_tendsto
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
:
∀ {x : MeasurableSpace β} [inst : MeasurableSpace γ] [inst_1 : Countable δ] {l : Filter δ}
[inst_2 : Filter.IsCountablyGenerated l] (l' : Filter γ) [inst_3 : Filter.IsCountablyGenerated l']
[hl' : Filter.IsMeasurablyGenerated l'] {f : δ → β → γ},
(∀ (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.
theorem
isCountablySpanning_measurableSet
{α : Type u_1}
[MeasurableSpace α]
:
IsCountablySpanning {s : Set α | MeasurableSet s}
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 : α) => { val := {a}, property := ⋯ } }
@[simp]
theorem
MeasurableSet.coe_singleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
(a : α)
:
↑{a} = {a}
instance
MeasurableSet.Subtype.instIsLawfulSingleton
{α : Type u_1}
[MeasurableSpace α]
[MeasurableSingletonClass α]
:
IsLawfulSingleton α (Subtype MeasurableSet)
Equations
- ⋯ = ⋯
@[simp]
@[simp]
theorem
MeasurableSet.coe_union
{α : Type u_1}
[MeasurableSpace α]
(s : Subtype MeasurableSet)
(t : Subtype MeasurableSet)
:
@[simp]
theorem
MeasurableSet.sup_eq_union
{α : Type u_1}
[MeasurableSpace α]
(s : { s : Set α // MeasurableSet s })
(t : { s : Set α // MeasurableSet s })
:
@[simp]
theorem
MeasurableSet.coe_inter
{α : Type u_1}
[MeasurableSpace α]
(s : Subtype MeasurableSet)
(t : Subtype MeasurableSet)
:
@[simp]
theorem
MeasurableSet.inf_eq_inter
{α : Type u_1}
[MeasurableSpace α]
(s : { s : Set α // MeasurableSet s })
(t : { s : Set α // MeasurableSet s })
:
@[simp]
theorem
MeasurableSet.coe_sdiff
{α : Type u_1}
[MeasurableSpace α]
(s : Subtype MeasurableSet)
(t : Subtype MeasurableSet)
:
Equations
- MeasurableSet.Subtype.instTop = { top := { val := Set.univ, property := ⋯ } }
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)