Measurable embeddings and equivalences #
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.
Main definitions #
MeasurableEmbedding: a mapf : α → βis called a measurable embedding if it is injective, measurable, and sends measurable sets to measurable sets.MeasurableEquiv: an equivalenceα ≃ βis a measurable equivalence if its forward and inverse functions are measurable.
We prove a multitude of elementary lemmas about these, and one more substantial theorem:
MeasurableEmbedding.schroederBernstein: the measurable Schröder-Bernstein Theorem: given measurable embeddingsα → βandβ → α, we can find a measurable equivalenceα ≃ᵐ β.
Notation #
- We write
α ≃ᵐ βfor measurable equivalences between the measurable spacesαandβ. This should not be confused with≃ₘwhich is used for diffeomorphisms between manifolds.
Tags #
measurable equivalence, measurable embedding
structure
MeasurableEmbedding
{α : Type u_1}
{β : Type u_2}
[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.
Instances For
theorem
MeasurableEmbedding.measurableSet_image
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{mα : MeasurableSpace α}
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
:
MeasurableSet (f '' s) ↔ MeasurableSet s
theorem
MeasurableEmbedding.id
{α : Type u_1}
{mα : MeasurableSpace α}
:
MeasurableEmbedding _root_.id
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}
{s : Set α}
{mα : MeasurableSpace α}
(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 : ∀ (a : β), 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
MeasurableEmbedding.natCast
{α : Type u_6}
[MeasurableSpace α]
[MeasurableSingletonClass α]
[AddMonoidWithOne α]
[CharZero α]
:
MeasurableEmbedding Nat.cast
theorem
MeasurableSet.of_union_range_cover
{α : Type u_1}
{α₁ : Type u_6}
{α₂ : Type u_7}
{mα : MeasurableSpace α}
{mα₁ : MeasurableSpace α₁}
{mα₂ : MeasurableSpace α₂}
{i₁ : α₁ → α}
{i₂ : α₂ → α}
{s : Set α}
(hi₁ : MeasurableEmbedding i₁)
(hi₂ : MeasurableEmbedding i₂)
(h : Set.univ ⊆ Set.range i₁ ∪ Set.range i₂)
(hs₁ : MeasurableSet (i₁ ⁻¹' s))
(hs₂ : MeasurableSet (i₂ ⁻¹' s))
:
theorem
MeasurableSet.of_union₃_range_cover
{α : Type u_1}
{α₁ : Type u_6}
{α₂ : Type u_7}
{α₃ : Type u_8}
{mα : MeasurableSpace α}
{mα₁ : MeasurableSpace α₁}
{mα₂ : MeasurableSpace α₂}
{mα₃ : MeasurableSpace α₃}
{i₁ : α₁ → α}
{i₂ : α₂ → α}
{i₃ : α₃ → α}
{s : Set α}
(hi₁ : MeasurableEmbedding i₁)
(hi₂ : MeasurableEmbedding i₂)
(hi₃ : MeasurableEmbedding i₃)
(h : Set.univ ⊆ Set.range i₁ ∪ Set.range i₂ ∪ Set.range i₃)
(hs₁ : MeasurableSet (i₁ ⁻¹' s))
(hs₂ : MeasurableSet (i₂ ⁻¹' s))
(hs₃ : MeasurableSet (i₃ ⁻¹' s))
:
theorem
Measurable.of_union_range_cover
{α : Type u_1}
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mα₁ : MeasurableSpace α₁}
{mα₂ : MeasurableSpace α₂}
{i₁ : α₁ → α}
{i₂ : α₂ → α}
{f : α → β}
(hi₁ : MeasurableEmbedding i₁)
(hi₂ : MeasurableEmbedding i₂)
(h : Set.univ ⊆ Set.range i₁ ∪ Set.range i₂)
(hf₁ : Measurable (f ∘ i₁))
(hf₂ : Measurable (f ∘ i₂))
:
theorem
Measurable.of_union₃_range_cover
{α : Type u_1}
{β : Type u_2}
{α₁ : Type u_6}
{α₂ : Type u_7}
{α₃ : Type u_8}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mα₁ : MeasurableSpace α₁}
{mα₂ : MeasurableSpace α₂}
{mα₃ : MeasurableSpace α₃}
{i₁ : α₁ → α}
{i₂ : α₂ → α}
{i₃ : α₃ → α}
{f : α → β}
(hi₁ : MeasurableEmbedding i₁)
(hi₂ : MeasurableEmbedding i₂)
(hi₃ : MeasurableEmbedding i₃)
(h : Set.univ ⊆ Set.range i₁ ∪ Set.range i₂ ∪ Set.range i₃)
(hf₁ : Measurable (f ∘ i₁))
(hf₂ : Measurable (f ∘ i₂))
(hf₃ : Measurable (f ∘ i₃))
:
theorem
MeasurableSet.exists_measurable_proj
{α : Type u_1}
{s : Set α}
{x✝ : MeasurableSpace α}
(hs : MeasurableSet s)
(hne : s.Nonempty)
:
∃ (f : α → ↑s), Measurable f ∧ ∀ (x : ↑s), f ↑x = x
structure
MeasurableEquiv
(α : Type u_6)
(β : Type u_7)
[MeasurableSpace α]
[MeasurableSpace β]
extends α ≃ β :
Type (max u_6 u_7)
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
- toFun : α → β
- invFun : β → α
- 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.
Instances For
Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.
Instances For
theorem
MeasurableEquiv.toEquiv_injective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
Function.Injective toEquiv
@[implicit_reducible]
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)
:
Any measurable space is equivalent to itself.
Instances For
@[implicit_reducible]
def
MeasurableEquiv.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
:
The composition of equivalences between measurable spaces.
Instances For
theorem
MeasurableEquiv.coe_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
:
⇑(ab.trans bc) = ⇑bc ∘ ⇑ab
def
MeasurableEquiv.symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(ab : α ≃ᵐ β)
:
The inverse of an equivalence between measurable spaces.
Instances For
@[simp]
theorem
MeasurableEquiv.coe_toEquiv_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
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.
Instances For
def
MeasurableEquiv.Simps.symm_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(h : α ≃ᵐ β)
:
β → α
See Note [custom simps projection]
Instances For
theorem
MeasurableEquiv.ext
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{e₁ e₂ : α ≃ᵐ β}
(h : ⇑e₁ = ⇑e₂)
:
e₁ = e₂
theorem
MeasurableEquiv.ext_iff
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{e₁ e₂ : α ≃ᵐ β}
:
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)
:
@[simp]
theorem
MeasurableEquiv.refl_toEquiv
(α : Type u_6)
[MeasurableSpace α]
:
(refl α).toEquiv = Equiv.refl α
@[simp]
theorem
MeasurableEquiv.trans_toEquiv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(ab : α ≃ᵐ β)
(bc : β ≃ᵐ γ)
:
@[simp]
@[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.symm_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.symm_bijective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
@[simp]
@[simp]
theorem
MeasurableEquiv.symm_comp_self
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
⇑e.symm ∘ ⇑e = id
@[simp]
theorem
MeasurableEquiv.self_comp_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
⇑e ∘ ⇑e.symm = id
@[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 : α ≃ᵐ β)
:
@[simp]
theorem
MeasurableEquiv.self_trans_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.surjective
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
Function.Surjective ⇑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 : α ≃ᵐ β)
:
Function.Injective ⇑e
@[simp]
theorem
MeasurableEquiv.symm_preimage_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(s : Set β)
:
theorem
MeasurableEquiv.image_eq_preimage_symm
{α : 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}
{s : Set α}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
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}
[i₁ : MeasurableSpace α]
[i₂ : MeasurableSpace β]
(h : α = β)
(hi : i₁ ≍ i₂)
:
Equal measurable spaces are equivalent.
Instances For
Measurable equivalence between ULift α and α.
Instances For
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.
Instances For
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.
Instances For
def
MeasurableEquiv.prodComm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
Products of measurable spaces are symmetric.
Instances For
def
MeasurableEquiv.prodAssoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
:
Products of measurable spaces are associative.
Instances For
PUnit is a left identity for product of measurable spaces up to a measurable equivalence.
Instances For
PUnit is a right identity for product of measurable spaces up to a measurable equivalence.
Instances For
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.
Instances For
def
MeasurableEquiv.Set.prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(s : Set α)
(t : Set β)
:
s ×ˢ t ≃ (s × t) as measurable spaces.
Instances For
univ α ≃ α as measurable spaces.
Instances For
{a} ≃ Unit as measurable spaces.
Instances For
def
MeasurableEquiv.Set.rangeInl
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
α is equivalent to its image in α ⊕ β as measurable spaces.
Instances For
def
MeasurableEquiv.Set.rangeInr
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
β is equivalent to its image in α ⊕ β as measurable spaces.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
def
MeasurableEquiv.subtypePiEquivPi
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
{p : (a : δ') → π a → Prop}
:
The type of functions f : ∀ a, β a such that for all a we have p a (f a) is measurably
equivalent to the type of functions ∀ a, {b : β a // p a b}.
Instances For
def
MeasurableEquiv.piCongrRight
{δ' : Type u_5}
{π : δ' → Type u_6}
{π' : δ' → Type u_7}
[(x : δ') → MeasurableSpace (π x)]
[(x : δ') → MeasurableSpace (π' x)]
(e : (a : δ') → π a ≃ᵐ π' a)
:
A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence
between Π a, β₁ a and Π a, β₂ a.
Instances For
def
MeasurableEquiv.piCongrLeft
{δ : Type u_4}
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
(f : δ ≃ δ')
:
Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.
Instances For
theorem
MeasurableEquiv.coe_piCongrLeft
{δ : Type u_4}
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
(f : δ ≃ δ')
:
⇑(piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)
theorem
MeasurableEquiv.piCongrLeft_apply_apply
{ι : Type u_8}
{ι' : Type u_9}
(e : ι ≃ ι')
{β : ι' → Type u_10}
[(i' : ι') → MeasurableSpace (β i')]
(x : (i : ι) → β (e i))
(i : ι)
:
(piCongrLeft (fun (i' : ι') => β i') e) x (e i) = x i
def
MeasurableEquiv.arrowProdEquivProdArrow
(α : Type u_8)
(β : Type u_9)
(γ : Type u_10)
[MeasurableSpace α]
[MeasurableSpace β]
:
The isomorphism (γ → α × β) ≃ (γ → α) × (γ → β) as a measurable equivalence.
Instances For
def
MeasurableEquiv.arrowCongr'
{α₁ : Type u_8}
{β₁ : Type u_9}
{α₂ : Type u_10}
{β₂ : Type u_11}
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(hα : α₁ ≃ α₂)
(hβ : β₁ ≃ᵐ β₂)
:
The measurable equivalence (α₁ → β₁) ≃ᵐ (α₂ → β₂) induced by α₁ ≃ α₂ and β₁ ≃ᵐ β₂.
Instances For
def
MeasurableEquiv.piMeasurableEquivTProd
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
[DecidableEq δ']
{l : List δ'}
(hnd : l.Nodup)
(h : ∀ (i : δ'), i ∈ l)
:
Pi-types are measurably equivalent to iterated products.
Instances For
@[simp]
theorem
MeasurableEquiv.piMeasurableEquivTProd_symm_apply
{δ' : Type u_5}
{π : δ' → Type u_6}
[(x : δ') → MeasurableSpace (π x)]
[DecidableEq δ']
{l : List δ'}
(hnd : l.Nodup)
(h : ∀ (i : δ'), i ∈ l)
:
⇑(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 : l.Nodup)
(h : ∀ (i : δ'), i ∈ l)
:
⇑(piMeasurableEquivTProd hnd h) = List.TProd.mk l
def
MeasurableEquiv.piUnique
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[Unique δ']
:
The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆ when the domain of π only contains ⋆
Instances For
@[simp]
theorem
MeasurableEquiv.piUnique_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[Unique δ']
:
@[simp]
theorem
MeasurableEquiv.piUnique_symm_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[Unique δ']
:
⇑(piUnique π).symm = uniqueElim
If α has a unique term, then the type of function α → β is measurably equivalent to β.
Instances For
@[simp]
theorem
MeasurableEquiv.funUnique_apply
(α : Type u_8)
(β : Type u_9)
[Unique α]
[MeasurableSpace β]
:
@[simp]
theorem
MeasurableEquiv.funUnique_symm_apply
(α : Type u_8)
(β : Type u_9)
[Unique α]
[MeasurableSpace β]
:
⇑(funUnique α β).symm = uniqueElim
The space Π i : Fin 2, α i is measurably equivalent to α 0 × α 1.
Instances For
@[simp]
theorem
MeasurableEquiv.piFinTwo_symm_apply
(α : Fin 2 → Type u_8)
[(i : Fin 2) → MeasurableSpace (α i)]
:
⇑(piFinTwo α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
@[simp]
theorem
MeasurableEquiv.piFinTwo_apply
(α : Fin 2 → Type u_8)
[(i : Fin 2) → MeasurableSpace (α i)]
:
⇑(piFinTwo α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)
The space Fin 2 → α is measurably equivalent to α × α.
Instances For
@[simp]
theorem
MeasurableEquiv.finTwoArrow_apply
{α : Type u_1}
[MeasurableSpace α]
:
⇑finTwoArrow = fun (f : Fin 2 → α) => (f 0, f 1)
@[simp]
theorem
MeasurableEquiv.finTwoArrow_symm_apply
{α : Type u_1}
[MeasurableSpace α]
:
⇑finTwoArrow.symm = fun (p : α × α) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
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).
Measurable version of Fin.insertNthEquiv.
Instances For
@[simp]
theorem
MeasurableEquiv.piFinSuccAbove_symm_apply
{n : ℕ}
(α : Fin (n + 1) → Type u_8)
[(i : Fin (n + 1)) → MeasurableSpace (α i)]
(i : Fin (n + 1))
:
⇑(piFinSuccAbove α i).symm = ⇑(Fin.insertNthEquiv α i)
@[simp]
theorem
MeasurableEquiv.piFinSuccAbove_apply
{n : ℕ}
(α : Fin (n + 1) → Type u_8)
[(i : Fin (n + 1)) → MeasurableSpace (α i)]
(i : Fin (n + 1))
:
⇑(piFinSuccAbove α i) = ⇑(Fin.insertNthEquiv α i).symm
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.
Instances For
@[simp]
theorem
MeasurableEquiv.piEquivPiSubtypeProd_symm_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
(p : δ' → Prop)
[DecidablePred p]
:
⇑(piEquivPiSubtypeProd π p).symm = fun (f : ((i : { x : δ' // p x }) → π ↑i) × ((i : { x : δ' // ¬p x }) → π ↑i)) (x : δ') =>
if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
@[simp]
theorem
MeasurableEquiv.piEquivPiSubtypeProd_apply
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
(p : δ' → Prop)
[DecidablePred p]
:
⇑(piEquivPiSubtypeProd π p) = fun (f : (i : δ') → π i) =>
(fun (x : { x : δ' // p x }) => f ↑x, fun (x : { x : δ' // ¬p x }) => f ↑x)
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.
Instances For
theorem
MeasurableEquiv.coe_sumPiEquivProdPi
{δ : Type u_4}
{δ' : Type u_5}
(α : δ ⊕ δ' → Type u_8)
[(i : δ ⊕ δ') → MeasurableSpace (α i)]
:
⇑(sumPiEquivProdPi α) = ⇑(Equiv.sumPiEquivProdPi α)
theorem
MeasurableEquiv.coe_sumPiEquivProdPi_symm
{δ : Type u_4}
{δ' : Type u_5}
(α : δ ⊕ δ' → Type u_8)
[(i : δ ⊕ δ') → MeasurableSpace (α i)]
:
⇑(sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm
def
MeasurableEquiv.piOptionEquivProd
{δ : Type u_8}
(α : Option δ → Type u_9)
[(i : Option δ) → MeasurableSpace (α i)]
:
The measurable equivalence for (dependent) functions on an Option type
(∀ i : Option δ, α i) ≃ᵐ (∀ (i : δ), α i) × α none.
Instances For
def
MeasurableEquiv.piFinsetUnion
{δ' : Type u_5}
(π : δ' → Type u_6)
[(x : δ') → MeasurableSpace (π x)]
[DecidableEq δ']
{s 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.
Instances For
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ᶜ.
Instances For
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.
Instances For
@[simp]
theorem
MeasurableEquiv.ofInvolutive_toEquiv
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(hf : Function.Involutive f)
(hf' : Measurable f)
:
(ofInvolutive f hf hf').toEquiv = Function.Involutive.toPerm f hf
@[simp]
theorem
MeasurableEquiv.ofInvolutive_apply
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(hf : Function.Involutive f)
(hf' : Measurable f)
(a : α)
:
(ofInvolutive f hf hf') a = f a
@[simp]
theorem
MeasurableEquiv.ofInvolutive_symm
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(hf : Function.Involutive f)
(hf' : Measurable f)
:
(ofInvolutive f hf hf').symm = ofInvolutive f hf hf'
setOf as a MeasurableEquiv.
Instances For
@[simp]
theorem
MeasurableEquiv.setOf_apply
{α : Type u_8}
(p : α → Prop)
:
MeasurableEquiv.setOf p = {a : α | p a}
@[simp]
theorem
MeasurableEquiv.setOf_symm_apply
{α : Type u_8}
(s : Set α)
(a : α)
:
MeasurableEquiv.setOf.symm s a = (a ∈ s)
@[simp]
@[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
Instances For
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
Instances For
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 α ≃ᵐ β.
Instances For
@[simp]
theorem
MeasurableEmbedding.equivRange_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
(x : α)
:
hf.equivRange x = ⟨f x, ⋯⟩
@[simp]
theorem
MeasurableEmbedding.equivRange_symm_apply_mk
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(hf : MeasurableEmbedding f)
(x : α)
:
hf.equivRange.symm ⟨f x, ⋯⟩ = x
noncomputable def
MeasurableEmbedding.invFun
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
[Nonempty α]
(hf : MeasurableEmbedding f)
(x : β)
:
α
The left-inverse of a MeasurableEmbedding
Instances For
theorem
MeasurableEmbedding.measurable_invFun
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
[Nonempty α]
(hf : MeasurableEmbedding f)
:
Measurable hf.invFun
theorem
MeasurableEmbedding.leftInverse_invFun
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
[Nonempty α]
(hf : MeasurableEmbedding f)
:
Function.LeftInverse hf.invFun f
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
Currying as a measurable equivalence #
def
MeasurableEquiv.piCurry
{ι : Type u_6}
{κ : ι → Type u_7}
(X : (i : ι) → κ i → Type u_8)
[(i : ι) → (j : κ i) → MeasurableSpace (X i j)]
:
The currying operation Function.curry as a measurable equivalence.
See MeasurableEquiv.curry for the non-dependent version.
Instances For
@[simp]
theorem
MeasurableEquiv.piCurry_apply
{ι : Type u_6}
{κ : ι → Type u_7}
(X : (i : ι) → κ i → Type u_8)
[(i : ι) → (j : κ i) → MeasurableSpace (X i j)]
(f : (x : (i : ι) × κ i) → X x.fst x.snd)
(x : ι)
(y : κ x)
:
(piCurry X) f x y = Sigma.curry f x y
@[simp]
theorem
MeasurableEquiv.piCurry_symm_apply
{ι : Type u_6}
{κ : ι → Type u_7}
(X : (i : ι) → κ i → Type u_8)
[(i : ι) → (j : κ i) → MeasurableSpace (X i j)]
(f : (x : ι) → (y : κ x) → X x y)
(x : Sigma κ)
:
(piCurry X).symm f x = Sigma.uncurry f x
theorem
MeasurableEquiv.coe_piCurry
{ι : Type u_6}
{κ : ι → Type u_7}
(X : (i : ι) → κ i → Type u_8)
[(i : ι) → (j : κ i) → MeasurableSpace (X i j)]
:
⇑(piCurry X) = Sigma.curry
theorem
MeasurableEquiv.coe_piCurry_symm
{ι : Type u_6}
{κ : ι → Type u_7}
(X : (i : ι) → κ i → Type u_8)
[(i : ι) → (j : κ i) → MeasurableSpace (X i j)]
:
⇑(piCurry X).symm = Sigma.uncurry
The currying operation Sigma.curry as a measurable equivalence.
See MeasurableEquiv.piCurry for the dependent version.
Instances For
@[simp]
theorem
MeasurableEquiv.curry_apply
(ι : Type u_6)
(κ : Type u_7)
(X : Type u_8)
[MeasurableSpace X]
(a✝ : ι × κ → X)
(a✝¹ : ι)
(a✝² : κ)
:
(curry ι κ X) a✝ a✝¹ a✝² = a✝ (a✝¹, a✝²)
@[simp]
theorem
MeasurableEquiv.curry_symm_apply
(ι : Type u_6)
(κ : Type u_7)
(X : Type u_8)
[MeasurableSpace X]
(a✝ : ι → κ → X)
(a✝¹ : ι × κ)
:
theorem
MeasurableEquiv.coe_curry
(ι : Type u_6)
(κ : Type u_7)
(X : Type u_8)
[MeasurableSpace X]
:
⇑(curry ι κ X) = Function.curry
theorem
MeasurableEquiv.coe_curry_symm
(ι : Type u_6)
(κ : Type u_7)
(X : Type u_8)
[MeasurableSpace X]
: