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
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 (Set.image f s)
The image of a measurable set under a measurable embedding is a measurable set.
Instances For
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 (DFunLike.coe self.toEquiv)
The forward function of a measurable equivalence is measurable.
- measurable_invFun : Measurable (DFunLike.coe 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.
Equations
- Eq «term_≃ᵐ_» (Lean.ParserDescr.trailingNode `«term_≃ᵐ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵐ ") (Lean.ParserDescr.cat `term 26)))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Any measurable space is equivalent to itself.
Equations
- Eq (MeasurableEquiv.refl α) { toEquiv := Equiv.refl α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Equations
- Eq MeasurableEquiv.instInhabited { default := MeasurableEquiv.refl α }
Instances For
The composition of equivalences between measurable spaces.
Equations
Instances For
The inverse of an equivalence between measurable spaces.
Instances For
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
Instances For
See Note [custom simps projection]
Equations
Instances For
A measurable equivalence is a measurable embedding.
Equal measurable spaces are equivalent.
Equations
- Eq (MeasurableEquiv.cast h hi) { toEquiv := Equiv.cast h, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Measurable equivalence between ULift α
and α
.
Equations
- Eq MeasurableEquiv.ulift { toEquiv := Equiv.ulift, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Any two types with unique elements are measurably equivalent.
Equations
- Eq (MeasurableEquiv.ofUniqueOfUnique α β) { toEquiv := Equiv.ofUnique α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products of equivalent measurable spaces are equivalent.
Equations
Instances For
Products of measurable spaces are symmetric.
Equations
- Eq MeasurableEquiv.prodComm { toEquiv := Equiv.prodComm α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products of measurable spaces are associative.
Equations
- Eq MeasurableEquiv.prodAssoc { toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
PUnit
is a left identity for product of measurable spaces up to a measurable equivalence.
Equations
- Eq MeasurableEquiv.punitProd { toEquiv := Equiv.punitProd α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
PUnit
is a right identity for product of measurable spaces up to a measurable equivalence.
Equations
- Eq MeasurableEquiv.prodPUnit { toEquiv := Equiv.prodPUnit α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Sums of measurable spaces are symmetric.
Equations
Instances For
s ×ˢ t ≃ (s × t)
as measurable spaces.
Equations
- Eq (MeasurableEquiv.Set.prod s t) { toEquiv := Equiv.Set.prod s t, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
univ α ≃ α
as measurable spaces.
Equations
- Eq (MeasurableEquiv.Set.univ α) { toEquiv := Equiv.Set.univ α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
{a} ≃ Unit
as measurable spaces.
Equations
- Eq (MeasurableEquiv.Set.singleton a) { toEquiv := Equiv.Set.singleton a, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
α
is equivalent to its image in α ⊕ β
as measurable spaces.
Equations
- Eq MeasurableEquiv.Set.rangeInl { toEquiv := Equiv.Set.rangeInl α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
β
is equivalent to its image in α ⊕ β
as measurable spaces.
Equations
- Eq MeasurableEquiv.Set.rangeInr { toEquiv := Equiv.Set.rangeInr α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products distribute over sums (on the right) as measurable spaces.
Equations
- Eq (MeasurableEquiv.sumProdDistrib α β γ) { toEquiv := Equiv.sumProdDistrib α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products distribute over sums (on the left) as measurable spaces.
Equations
Instances For
Products distribute over sums as measurable spaces.
Equations
- Eq (MeasurableEquiv.sumProdSum α β γ δ) ((MeasurableEquiv.sumProdDistrib α β (Sum γ δ)).trans ((MeasurableEquiv.prodSumDistrib α γ δ).sumCongr (MeasurableEquiv.prodSumDistrib β γ δ)))
Instances For
A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a
generates a measurable equivalence
between Π a, β₁ a
and Π a, β₂ a
.
Equations
- Eq (MeasurableEquiv.piCongrRight e) { toEquiv := Equiv.piCongrRight fun (a : δ') => (e a).toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.
Equations
- Eq (MeasurableEquiv.piCongrLeft π f) { toEquiv := Equiv.piCongrLeft π f, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The isomorphism (γ → α × β) ≃ (γ → α) × (γ → β)
as a measurable equivalence.
Equations
- Eq (MeasurableEquiv.arrowProdEquivProdArrow α β γ) { toEquiv := Equiv.arrowProdEquivProdArrow γ (fun (i : γ) => α) fun (i : γ) => β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The measurable equivalence (α₁ → β₁) ≃ᵐ (α₂ → β₂)
induced by α₁ ≃ α₂
and β₁ ≃ᵐ β₂
.
Equations
- Eq (MeasurableEquiv.arrowCongr' hα hβ) { toEquiv := hα.arrowCongr' (EquivLike.toEquiv hβ), measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Pi-types are measurably equivalent to iterated products.
Equations
- Eq (MeasurableEquiv.piMeasurableEquivTProd hnd h) { toEquiv := List.TProd.piEquivTProd hnd h, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆
when the domain of π
only contains ⋆
Equations
- Eq (MeasurableEquiv.piUnique π) { toEquiv := Equiv.piUnique π, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
If α
has a unique term, then the type of function α → β
is measurably equivalent to β
.
Equations
- Eq (MeasurableEquiv.funUnique α β) (MeasurableEquiv.piUnique fun (a : α) => β)
Instances For
The space Π i : Fin 2, α i
is measurably equivalent to α 0 × α 1
.
Equations
- Eq (MeasurableEquiv.piFinTwo α) { toEquiv := piFinTwoEquiv α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The space Fin 2 → α
is measurably equivalent to α × α
.
Equations
- Eq MeasurableEquiv.finTwoArrow (MeasurableEquiv.piFinTwo fun (x : Fin 2) => α)
Instances For
Measurable equivalence between Π j : Fin (n + 1), α j
and
α i × Π j : Fin n, α (Fin.succAbove i j)
.
Measurable version of Fin.insertNthEquiv
.
Equations
- Eq (MeasurableEquiv.piFinSuccAbove α i) { toEquiv := (Fin.insertNthEquiv α i).symm, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
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
- Eq (MeasurableEquiv.piEquivPiSubtypeProd π p) { toEquiv := Equiv.piEquivPiSubtypeProd p π, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The measurable equivalence between the pi type over a sum type and a product of pi-types.
This is similar to MeasurableEquiv.piEquivPiSubtypeProd
.
Equations
- Eq (MeasurableEquiv.sumPiEquivProdPi α) { toEquiv := Equiv.sumPiEquivProdPi α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
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
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
If s
is a measurable set in a measurable space, that space is equivalent
to the sum of s
and sᶜ
.
Equations
- Eq (MeasurableEquiv.sumCompl hs) { toEquiv := Equiv.sumCompl fun (x : α) => Membership.mem s x, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Convert a measurable involutive function f
to a measurable permutation with
toFun = invFun = f
. See also Function.Involutive.toPerm
.
Equations
- Eq (MeasurableEquiv.ofInvolutive f hf hf') { toEquiv := Function.Involutive.toPerm f hf, measurable_toFun := hf', measurable_invFun := hf' }
Instances For
A set is equivalent to its image under a function f
as measurable spaces,
if f
is a measurable embedding
Equations
- Eq (MeasurableEmbedding.equivImage s hf) { toEquiv := Equiv.Set.image f s ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The domain of f
is equivalent to its range as measurable spaces,
if f
is a measurable embedding
Equations
- Eq hf.equivRange ((MeasurableEquiv.Set.univ α).symm.trans ((MeasurableEmbedding.equivImage Set.univ hf).trans (MeasurableEquiv.cast ⋯ ⋯)))
Instances For
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.