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 (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 ⇑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.
Equations
- «term_≃ᵐ_» = Lean.ParserDescr.trailingNode `«term_≃ᵐ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵐ ") (Lean.ParserDescr.cat `term 26))
Instances For
Any measurable space is equivalent to itself.
Equations
- MeasurableEquiv.refl α = { toEquiv := Equiv.refl α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Equations
- MeasurableEquiv.instInhabited = { default := MeasurableEquiv.refl α }
The composition of equivalences between measurable spaces.
Equations
- ab.trans bc = { toEquiv := ab.trans bc.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The inverse of an equivalence between measurable spaces.
Equations
- ab.symm = { toEquiv := ab.symm, measurable_toFun := ⋯, measurable_invFun := ⋯ }
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
- MeasurableEquiv.Simps.symm_apply h = ⇑h.symm
Instances For
A measurable equivalence is a measurable embedding.
Equal measurable spaces are equivalent.
Equations
- MeasurableEquiv.cast h hi = { toEquiv := Equiv.cast h, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Any two types with unique elements are measurably equivalent.
Equations
- MeasurableEquiv.ofUniqueOfUnique α β = { toEquiv := Equiv.equivOfUnique α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products of equivalent measurable spaces are equivalent.
Equations
- ab.prodCongr cd = { toEquiv := ab.prodCongr cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products of measurable spaces are symmetric.
Equations
- MeasurableEquiv.prodComm = { toEquiv := Equiv.prodComm α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products of measurable spaces are associative.
Equations
- 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
- 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
- MeasurableEquiv.prodPUnit = { toEquiv := Equiv.prodPUnit α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Sums of measurable spaces are symmetric.
Equations
- ab.sumCongr cd = { toEquiv := ab.sumCongr cd.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
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
univ α ≃ α
as measurable spaces.
Equations
- MeasurableEquiv.Set.univ α = { toEquiv := Equiv.Set.univ α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
{a} ≃ Unit
as measurable spaces.
Equations
- 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
- MeasurableEquiv.Set.rangeInl = { toEquiv := Equiv.Set.rangeInl α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
β
is equivalent to its image in α ⊕ β
as measurable spaces.
Equations
- MeasurableEquiv.Set.rangeInr = { toEquiv := Equiv.Set.rangeInr α β, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
Products distribute over sums (on the right) as measurable spaces.
Equations
- MeasurableEquiv.sumProdDistrib α β γ = { toEquiv := Equiv.sumProdDistrib α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
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
Products distribute over sums as measurable spaces.
Equations
- MeasurableEquiv.sumProdSum α β γ δ = (MeasurableEquiv.sumProdDistrib α β (γ ⊕ δ)).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
- 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
- MeasurableEquiv.piCongrLeft π f = { toEquiv := Equiv.piCongrLeft π f, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The isomorphism (γ → α × β) ≃ (γ → α) × (γ → β)
as a measurable equivalence.
Equations
- MeasurableEquiv.arrowProdEquivProdArrow α β γ = { toEquiv := Equiv.arrowProdEquivProdArrow α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The measurable equivalence (α₁ → β₁) ≃ᵐ (α₂ → β₂)
induced by α₁ ≃ α₂
and β₁ ≃ᵐ β₂
.
Equations
- MeasurableEquiv.arrowCongr' hα hβ = { toEquiv := hα.arrowCongr' ↑hβ, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
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
The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆
when the domain of π
only contains ⋆
Equations
- 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
- MeasurableEquiv.funUnique α β = MeasurableEquiv.piUnique fun (a : α) => β
Instances For
The space Π i : Fin 2, α i
is measurably equivalent to α 0 × α 1
.
Equations
- MeasurableEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
The space Fin 2 → α
is measurably equivalent to α × α
.
Equations
- 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
- 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
- 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
- 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
- MeasurableEquiv.sumCompl hs = { toEquiv := Equiv.sumCompl fun (x : α) => x ∈ s, 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
- 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
- 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
- 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.