# 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 map `f : α → β` 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

source
structure MeasurableEmbedding {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) :
Prop

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

source
theorem MeasurableEmbedding.measurableSet_image {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :
MeasurableSet (f '' s) ↔ MeasurableSet s
source
theorem MeasurableEmbedding.id {α : Type u_1} {mα : MeasurableSpace α} :
MeasurableEmbedding _root_.id
source
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)
source
theorem MeasurableEmbedding.subtype_coe {α : Type u_1} {s : Set α} {mα : MeasurableSpace α} (hs : MeasurableSet s) :
MeasurableEmbedding Subtype.val
source
theorem MeasurableEmbedding.measurableSet_range {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :
MeasurableSet (Set.range f)
source
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)
source
theorem MeasurableEmbedding.measurable_rangeSplitting {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :
Measurable (Set.rangeSplitting f)
source
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')
source
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
source
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
source
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)) :
MeasurableSet s
source
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)) :
MeasurableSet s
source
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₂)) :
Measurable f
source
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₃)) :
Measurable f
source
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
source
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 : β → α
- 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.

Instances For

source
def «term_≃ᵐ_» :
Lean.TrailingParserDescr

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))

Instances For

source
theorem MeasurableEquiv.toEquiv_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
Function.Injective toEquiv
source
instance MeasurableEquiv.instEquivLike {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
EquivLike (α ≃ᵐ β) α β
Equations

- MeasurableEquiv.instEquivLike = { coe := fun (e : α ≃ᵐ β) => ⇑e.toEquiv, inv := fun (e : α ≃ᵐ β) => ⇑e.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source
@[simp]
theorem MeasurableEquiv.coe_toEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
⇑e.toEquiv = ⇑e
source
theorem MeasurableEquiv.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
Measurable ⇑e
source
@[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
source
def MeasurableEquiv.refl (α : Type u_6) [MeasurableSpace α] :
α ≃ᵐ α

Any measurable space is equivalent to itself.

Equations

- MeasurableEquiv.refl α = { toEquiv := Equiv.refl α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
instance MeasurableEquiv.instInhabited {α : Type u_1} [MeasurableSpace α] :
Inhabited (α ≃ᵐ α)
Equations

- MeasurableEquiv.instInhabited = { default := MeasurableEquiv.refl α }

source
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 := ⋯ }

Instances For

source
theorem MeasurableEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
⇑(ab.trans bc) = ⇑bc ∘ ⇑ab
source
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 := ⋯ }

Instances For

source
@[simp]
theorem MeasurableEquiv.coe_toEquiv_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
⇑e.symm = ⇑e.symm
source
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

- MeasurableEquiv.Simps.apply h = ⇑h

Instances For

source
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

Instances For

source
theorem MeasurableEquiv.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ e₂ : α ≃ᵐ β} (h : ⇑e₁ = ⇑e₂) :
e₁ = e₂
source
theorem MeasurableEquiv.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ e₂ : α ≃ᵐ β} :
e₁ = e₂ ↔ ⇑e₁ = ⇑e₂
source
@[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 }
source
@[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✝)
source
@[simp]
theorem MeasurableEquiv.refl_toEquiv (α : Type u_6) [MeasurableSpace α] :
(refl α).toEquiv = Equiv.refl α
source
@[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
source
@[simp]
theorem MeasurableEquiv.refl_apply (α : Type u_6) [MeasurableSpace α] (a : α) :
(refl α) a = a
source
@[simp]
theorem MeasurableEquiv.symm_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
e.symm.symm = e
source
theorem MeasurableEquiv.symm_bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
Function.Bijective symm
source
@[simp]
theorem MeasurableEquiv.symm_refl (α : Type u_6) [MeasurableSpace α] :
(refl α).symm = refl α
source
@[simp]
theorem MeasurableEquiv.symm_comp_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
⇑e.symm ∘ ⇑e = id
source
@[simp]
theorem MeasurableEquiv.self_comp_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
⇑e ∘ ⇑e.symm = id
source
@[simp]
theorem MeasurableEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (y : β) :
e (e.symm y) = y
source
@[simp]
theorem MeasurableEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (x : α) :
e.symm (e x) = x
source
@[simp]
theorem MeasurableEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
e.symm.trans e = refl β
source
@[simp]
theorem MeasurableEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
e.trans e.symm = refl α
source
theorem MeasurableEquiv.surjective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
Function.Surjective ⇑e
source
theorem MeasurableEquiv.bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
Function.Bijective ⇑e
source
theorem MeasurableEquiv.injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
Function.Injective ⇑e
source
@[simp]
theorem MeasurableEquiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s
source
theorem MeasurableEquiv.image_eq_preimage_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
⇑e '' s = ⇑e.symm ⁻¹' s
source
theorem MeasurableEquiv.preimage_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
⇑e.symm ⁻¹' s = ⇑e '' s
source
theorem MeasurableEquiv.image_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
⇑e.symm '' s = ⇑e ⁻¹' s
source
theorem MeasurableEquiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) (t : Set α) :
s = ⇑e '' t ↔ ⇑e.symm '' s = t
source
@[simp]
theorem MeasurableEquiv.image_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
⇑e '' (⇑e ⁻¹' s) = s
source
@[simp]
theorem MeasurableEquiv.preimage_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
⇑e ⁻¹' (⇑e '' s) = s
source
@[simp]
theorem MeasurableEquiv.measurableSet_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) {s : Set β} :
MeasurableSet (⇑e ⁻¹' s) ↔ MeasurableSet s
source
@[simp]
theorem MeasurableEquiv.measurableSet_image {α : Type u_1} {β : Type u_2} {s : Set α} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
MeasurableSet (⇑e '' s) ↔ MeasurableSet s
source
@[simp]
theorem MeasurableEquiv.map_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
MeasurableSpace.map (⇑e) inst✝ = inst✝¹
source
theorem MeasurableEquiv.measurableEmbedding {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
MeasurableEmbedding ⇑e

A measurable equivalence is a measurable embedding.

source
def MeasurableEquiv.cast {α β : Type u_6} [i₁ : MeasurableSpace α] [i₂ : MeasurableSpace β] (h : α = β) (hi : i₁ ≍ i₂) :
α ≃ᵐ β

Equal measurable spaces are equivalent.

Equations

- MeasurableEquiv.cast h hi = { toEquiv := Equiv.cast h, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.ulift {α : Type u} [MeasurableSpace α] :
ULift.{v, u} α ≃ᵐ α

Measurable equivalence between `ULift α` and `α`.

Equations

- MeasurableEquiv.ulift = { toEquiv := Equiv.ulift, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
theorem MeasurableEquiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : β → γ} (e : α ≃ᵐ β) :
Measurable (f ∘ ⇑e) ↔ Measurable f
source
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.ofUnique α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
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

- ab.prodCongr cd = { toEquiv := ab.prodCongr cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
def MeasurableEquiv.punitProd {α : Type u_1} [MeasurableSpace α] :
PUnit.{u_6 + 1} × α ≃ᵐ α

`PUnit` is a left identity for product of measurable spaces up to a measurable equivalence.

Equations

- MeasurableEquiv.punitProd = { toEquiv := Equiv.punitProd α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.prodPUnit {α : Type u_1} [MeasurableSpace α] :
α × PUnit.{u_6 + 1} ≃ᵐ α

`PUnit` is a right identity for product of measurable spaces up to a measurable equivalence.

Equations

- MeasurableEquiv.prodPUnit = { toEquiv := Equiv.prodPUnit α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
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

- ab.sumCongr cd = { toEquiv := ab.sumCongr cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.Set.prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (s : Set α) (t : Set β) :
↑(s ×ˢ t) ≃ᵐ ↑s × ↑t

`s ×ˢ t ≃ (s × t)` as measurable spaces.

Equations

- MeasurableEquiv.Set.prod s t = { toEquiv := Equiv.Set.prod s t, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.Set.univ (α : Type u_6) [MeasurableSpace α] :
↑_root_.Set.univ ≃ᵐ α

`univ α ≃ α` as measurable spaces.

Equations

- MeasurableEquiv.Set.univ α = { toEquiv := Equiv.Set.univ α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.Set.singleton {α : Type u_1} [MeasurableSpace α] (a : α) :
↑{a} ≃ᵐ Unit

`{a} ≃ Unit` as measurable spaces.

Equations

- MeasurableEquiv.Set.singleton a = { toEquiv := Equiv.Set.singleton a, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.Set.rangeInl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
↑(Set.range Sum.inl) ≃ᵐ α

`α` is equivalent to its image in `α ⊕ β` as measurable spaces.

Equations

- MeasurableEquiv.Set.rangeInl = { toEquiv := Equiv.Set.rangeInl α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.Set.rangeInr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
↑(Set.range Sum.inr) ≃ᵐ β

`β` is equivalent to its image in `α ⊕ β` as measurable spaces.

Equations

- MeasurableEquiv.Set.rangeInr = { toEquiv := Equiv.Set.rangeInr α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
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

- MeasurableEquiv.prodSumDistrib α β γ = MeasurableEquiv.prodComm.trans ((MeasurableEquiv.sumProdDistrib β γ α).trans (MeasurableEquiv.prodComm.sumCongr MeasurableEquiv.prodComm))

Instances For

source
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.prodSumDistrib α γ δ).sumCongr (MeasurableEquiv.prodSumDistrib β γ δ))

Instances For

source
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 := ⋯ }

Instances For

source
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 = { toEquiv := Equiv.piCongrLeft π f, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
theorem MeasurableEquiv.coe_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] (f : δ ≃ δ') :
⇑(piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)
source
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
source
def MeasurableEquiv.arrowProdEquivProdArrow (α : Type u_8) (β : Type u_9) (γ : Type u_10) [MeasurableSpace α] [MeasurableSpace β] :
(γ → α × β) ≃ᵐ (γ → α) × (γ → β)

The isomorphism `(γ → α × β) ≃ (γ → α) × (γ → β)` as a measurable equivalence.

Equations

- MeasurableEquiv.arrowProdEquivProdArrow α β γ = { toEquiv := Equiv.arrowProdEquivProdArrow γ (fun (i : γ) => α) fun (i : γ) => β, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
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 `β₁ ≃ᵐ β₂`.

Equations

- MeasurableEquiv.arrowCongr' hα hβ = { toEquiv := hα.arrowCongr' ↑hβ, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
def MeasurableEquiv.piMeasurableEquivTProd {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (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 := ⋯ }

Instances For

source
@[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
source
@[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
source
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 := ⋯ }

Instances For

source
@[simp]
theorem MeasurableEquiv.piUnique_symm_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
⇑(piUnique π).symm = uniqueElim
source
@[simp]
theorem MeasurableEquiv.piUnique_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
⇑(piUnique π) = fun (f : (i : δ') → π i) => f default
source
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 : α) => β

Instances For

source
@[simp]
theorem MeasurableEquiv.funUnique_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
⇑(funUnique α β) = fun (f : α → β) => f default
source
@[simp]
theorem MeasurableEquiv.funUnique_symm_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
⇑(funUnique α β).symm = uniqueElim
source
def MeasurableEquiv.piFinTwo (α : Fin 2 → Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
((i : Fin 2) → α i) ≃ᵐ α 0 × α 1

The space `Π i : Fin 2, α i` is measurably equivalent to `α 0 × α 1`.

Equations

- MeasurableEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
@[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)
source
@[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)
source
def MeasurableEquiv.finTwoArrow {α : Type u_1} [MeasurableSpace α] :
(Fin 2 → α) ≃ᵐ α × α

The space `Fin 2 → α` is measurably equivalent to `α × α`.

Equations

- MeasurableEquiv.finTwoArrow = MeasurableEquiv.piFinTwo fun (x : Fin 2) => α

Instances For

source
@[simp]
theorem MeasurableEquiv.finTwoArrow_symm_apply {α : Type u_1} [MeasurableSpace α] :
⇑finTwoArrow.symm = fun (p : α × α) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
source
@[simp]
theorem MeasurableEquiv.finTwoArrow_apply {α : Type u_1} [MeasurableSpace α] :
⇑finTwoArrow = fun (f : Fin 2 → α) => (f 0, f 1)
source
def MeasurableEquiv.piFinSuccAbove {n : ℕ} (α : Fin (n + 1) → Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
((j : Fin (n + 1)) → α j) ≃ᵐ α i × ((j : Fin n) → α (i.succAbove j))

Measurable equivalence between `Π j : Fin (n + 1), α j` and `α i × Π j : Fin n, α (Fin.succAbove i j)`.

Measurable version of `Fin.insertNthEquiv`.

Equations

- MeasurableEquiv.piFinSuccAbove α i = { toEquiv := (Fin.insertNthEquiv α i).symm, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
@[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
source
@[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)
source
def MeasurableEquiv.piEquivPiSubtypeProd {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ' → Prop) [DecidablePred p] :
((i : δ') → π i) ≃ᵐ ((i : Subtype p) → π ↑i) × ((i : { i : δ' // ¬p i }) → π ↑i)

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 := ⋯ }

Instances For

source
@[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)
source
@[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⟩
source
def MeasurableEquiv.sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [(i : δ ⊕ δ') → MeasurableSpace (α i)] :
((i : δ ⊕ δ') → α i) ≃ᵐ ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr 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 α = { toEquiv := Equiv.sumPiEquivProdPi α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
theorem MeasurableEquiv.coe_sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [(i : δ ⊕ δ') → MeasurableSpace (α i)] :
⇑(sumPiEquivProdPi α) = ⇑(Equiv.sumPiEquivProdPi α)
source
theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [(i : δ ⊕ δ') → MeasurableSpace (α i)] :
⇑(sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm
source
def MeasurableEquiv.piOptionEquivProd {δ : Type u_8} (α : Option δ → Type u_9) [(i : Option δ) → MeasurableSpace (α i)] :
((i : Option δ) → α i) ≃ᵐ ((i : δ) → α (some i)) × α none

The measurable equivalence for (dependent) functions on an Option type `(∀ i : Option δ, α i) ≃ᵐ (∀ (i : δ), α i) × α none`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def MeasurableEquiv.piFinsetUnion {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {s t : Finset δ'} (h : Disjoint s t) :
((i : ↥s) → π ↑i) × ((i : ↥t) → π ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → π ↑i)

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.

Instances For

source
def MeasurableEquiv.sumCompl {α : Type u_1} [MeasurableSpace α] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) :
↑s ⊕ ↑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 := ⋯ }

Instances For

source
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' }

Instances For

source
@[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
source
@[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
source
@[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'
source
def MeasurableEquiv.setOf {α : Type u_8} :
(α → Prop) ≃ᵐ Set α

`setOf` as a `MeasurableEquiv`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem MeasurableEquiv.setOf_symm_apply {α : Type u_8} (s : Set α) (a : α) :
MeasurableEquiv.setOf.symm s a = (a ∈ s)
source
@[simp]
theorem MeasurableEquiv.setOf_apply {α : Type u_8} (p : α → Prop) :
MeasurableEquiv.setOf p = {a : α | p a}
source
@[simp]
theorem MeasurableEquiv.coe_setOf {α : Type u_8} :
⇑MeasurableEquiv.setOf = setOf
source
@[simp]
theorem MeasurableEmbedding.comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :
MeasurableSpace.comap f inst✝ = inst✝¹
source
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)
source
noncomputable def MeasurableEmbedding.equivImage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (s : Set α) (hf : MeasurableEmbedding f) :
↑s ≃ᵐ ↑(f '' s)

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 := ⋯ }

Instances For

source
noncomputable def MeasurableEmbedding.equivRange {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :
α ≃ᵐ ↑(Set.range f)

The domain of `f` is equivalent to its range as measurable spaces, if `f` is a measurable embedding

Equations

- hf.equivRange = (MeasurableEquiv.Set.univ α).symm.trans ((MeasurableEmbedding.equivImage Set.univ hf).trans (MeasurableEquiv.cast ⋯ ⋯))

Instances For

source
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)) :
MeasurableEmbedding f
source
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) :
MeasurableEmbedding f
source
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.

Instances For

source
@[simp]
theorem MeasurableEmbedding.equivRange_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) (x : α) :
hf.equivRange x = ⟨f x, ⋯⟩
source
@[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
source
noncomputable def MeasurableEmbedding.invFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} [Nonempty α] (hf : MeasurableEmbedding f) (x : β) :
α

The left-inverse of a `MeasurableEmbedding`

Equations

- hf.invFun x = if hx : x ∈ Set.range f then hf.equivRange.symm ⟨x, hx⟩ else ⋯.some

Instances For

source
theorem MeasurableEmbedding.measurable_invFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} [Nonempty α] (hf : MeasurableEmbedding f) :
Measurable hf.invFun
source
theorem MeasurableEmbedding.leftInverse_invFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} [Nonempty α] (hf : MeasurableEmbedding f) :
Function.LeftInverse hf.invFun f
source
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
source
@[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 #

source
def MeasurableEquiv.piCurry {ι : Type u_6} {κ : ι → Type u_7} (X : (i : ι) → κ i → Type u_8) [(i : ι) → (j : κ i) → MeasurableSpace (X i j)] :
((p : (i : ι) × κ i) → X p.fst p.snd) ≃ᵐ ((i : ι) → (j : κ i) → X i j)

The currying operation `Function.curry` as a measurable equivalence. See `MeasurableEquiv.curry` for the non-dependent version.

Equations

- MeasurableEquiv.piCurry X = { toEquiv := Equiv.piCurry X, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
@[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
source
@[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
source
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
source
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
source
def MeasurableEquiv.curry (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [MeasurableSpace X] :
(ι × κ → X) ≃ᵐ (ι → κ → X)

The currying operation `Sigma.curry` as a measurable equivalence. See `MeasurableEquiv.piCurry` for the dependent version.

Equations

- MeasurableEquiv.curry ι κ X = { toEquiv := Equiv.curry ι κ X, measurable_toFun := ⋯, measurable_invFun := ⋯ }

Instances For

source
@[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✝²)
source
@[simp]
theorem MeasurableEquiv.curry_symm_apply (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [MeasurableSpace X] (a✝ : ι → κ → X) (a✝¹ : ι × κ) :
(curry ι κ X).symm a✝ a✝¹ = Function.uncurry a✝ a✝¹
source
theorem MeasurableEquiv.coe_curry (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [MeasurableSpace X] :
⇑(curry ι κ X) = Function.curry
source
theorem MeasurableEquiv.coe_curry_symm (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [MeasurableSpace X] :
⇑(curry ι κ X).symm = Function.uncurry