Documentation

Mathlib.MeasureTheory.MeasurableSpace.Embedding

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 #

We prove a multitude of elementary lemmas about these, and one more substantial theorem:

Notation #

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.

Instances For
    theorem MeasurableEmbedding.measurableSet_image {α : Type u_1} {β : Type u_2} {s : Set α} { : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
    theorem MeasurableEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {g : βγ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
    theorem MeasurableEmbedding.measurableSet_range {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
    theorem MeasurableEmbedding.measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} (hf : MeasurableEmbedding f) {g : αγ} {g' : βγ} (hg : Measurable g) (hg' : Measurable g') :
    theorem MeasurableEmbedding.exists_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} (hf : MeasurableEmbedding f) {g : αγ} (hg : Measurable g) (hne : βNonempty γ) :
    Exists fun (g' : βγ) => And (Measurable g') (Eq (Function.comp g' f) g)
    theorem MeasurableEmbedding.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} { : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {g : βγ} (hg : MeasurableEmbedding g) :
    theorem MeasurableSet.of_union_range_cover {α : Type u_1} {α₁ : Type u_6} {α₂ : Type u_7} { : MeasurableSpace α} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {i₁ : α₁α} {i₂ : α₂α} {s : Set α} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (h : HasSubset.Subset Set.univ (Union.union (Set.range i₁) (Set.range i₂))) (hs₁ : MeasurableSet (Set.preimage i₁ s)) (hs₂ : MeasurableSet (Set.preimage i₂ s)) :
    theorem MeasurableSet.of_union₃_range_cover {α : Type u_1} {α₁ : Type u_6} {α₂ : Type u_7} {α₃ : Type u_8} { : MeasurableSpace α} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {mα₃ : MeasurableSpace α₃} {i₁ : α₁α} {i₂ : α₂α} {i₃ : α₃α} {s : Set α} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (hi₃ : MeasurableEmbedding i₃) (h : HasSubset.Subset Set.univ (Union.union (Union.union (Set.range i₁) (Set.range i₂)) (Set.range i₃))) (hs₁ : MeasurableSet (Set.preimage i₁ s)) (hs₂ : MeasurableSet (Set.preimage i₂ s)) (hs₃ : MeasurableSet (Set.preimage i₃ s)) :
    theorem Measurable.of_union_range_cover {α : Type u_1} {β : Type u_2} {α₁ : Type u_6} {α₂ : Type u_7} { : MeasurableSpace α} { : MeasurableSpace β} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {i₁ : α₁α} {i₂ : α₂α} {f : αβ} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (h : HasSubset.Subset Set.univ (Union.union (Set.range i₁) (Set.range i₂))) (hf₁ : Measurable (Function.comp f i₁)) (hf₂ : Measurable (Function.comp f i₂)) :
    theorem Measurable.of_union₃_range_cover {α : Type u_1} {β : Type u_2} {α₁ : Type u_6} {α₂ : Type u_7} {α₃ : Type u_8} { : MeasurableSpace α} { : MeasurableSpace β} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {mα₃ : MeasurableSpace α₃} {i₁ : α₁α} {i₂ : α₂α} {i₃ : α₃α} {f : αβ} (hi₁ : MeasurableEmbedding i₁) (hi₂ : MeasurableEmbedding i₂) (hi₃ : MeasurableEmbedding i₃) (h : HasSubset.Subset Set.univ (Union.union (Union.union (Set.range i₁) (Set.range i₂)) (Set.range i₃))) (hf₁ : Measurable (Function.comp f i₁)) (hf₂ : Measurable (Function.comp f i₂)) (hf₃ : Measurable (Function.comp f i₃)) :
    theorem MeasurableSet.exists_measurable_proj {α : Type u_1} {s : Set α} {x✝ : MeasurableSpace α} (hs : MeasurableSet s) (hne : s.Nonempty) :
    Exists fun (f : αs.Elem) => And (Measurable f) (∀ (x : s.Elem), Eq (f x.val) x)
    structure MeasurableEquiv (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] extends Equiv α β :
    Type (max u_6 u_7)

    Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

    Instances For

      Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem MeasurableEquiv.coe_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : Equiv α β) (h1 : Measurable (DFunLike.coe e)) (h2 : Measurable (DFunLike.coe e.symm)) :
          Eq (DFunLike.coe { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }) (DFunLike.coe e)

          Any measurable space is equivalent to itself.

          Equations
          Instances For
            def MeasurableEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) :

            The composition of equivalences between measurable spaces.

            Equations
            • Eq (ab.trans bc) { toEquiv := ab.trans bc.toEquiv, measurable_toFun := , measurable_invFun := }
            Instances For
              theorem MeasurableEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) :
              def MeasurableEquiv.symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (ab : MeasurableEquiv α β) :

              The inverse of an equivalence between measurable spaces.

              Equations
              • Eq ab.symm { toEquiv := ab.symm, measurable_toFun := , measurable_invFun := }
              Instances For
                def MeasurableEquiv.Simps.apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : MeasurableEquiv α β) :
                αβ

                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
                  def MeasurableEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : MeasurableEquiv α β) :
                  βα

                  See Note [custom simps projection]

                  Equations
                  Instances For
                    theorem MeasurableEquiv.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ e₂ : MeasurableEquiv α β} (h : Eq (DFunLike.coe e₁) (DFunLike.coe e₂)) :
                    Eq e₁ e₂
                    theorem MeasurableEquiv.ext_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ e₂ : MeasurableEquiv α β} :
                    Iff (Eq e₁ e₂) (Eq (DFunLike.coe e₁) (DFunLike.coe e₂))
                    theorem MeasurableEquiv.symm_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : Equiv α β) (h1 : Measurable (DFunLike.coe e)) (h2 : Measurable (DFunLike.coe e.symm)) :
                    Eq { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }
                    theorem MeasurableEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) (a✝ : α) :
                    Eq (DFunLike.coe (ab.trans bc) a✝) (DFunLike.coe bc (DFunLike.coe ab a✝))
                    theorem MeasurableEquiv.refl_apply (α : Type u_6) [MeasurableSpace α] (a : α) :
                    Eq (DFunLike.coe (refl α) a) a
                    theorem MeasurableEquiv.trans_toEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : MeasurableEquiv α β) (bc : MeasurableEquiv β γ) :
                    Eq (ab.trans bc).toEquiv (ab.trans bc.toEquiv)
                    theorem MeasurableEquiv.symm_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) :
                    theorem MeasurableEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (y : β) :
                    theorem MeasurableEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (x : α) :
                    theorem MeasurableEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) :
                    Eq (e.symm.trans e) (refl β)
                    theorem MeasurableEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) :
                    Eq (e.trans e.symm) (refl α)
                    theorem MeasurableEquiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) (s : Set β) (t : Set α) :
                    theorem MeasurableEquiv.map_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : MeasurableEquiv α β) :
                    Eq (MeasurableSpace.map (DFunLike.coe e) inst✝) inst✝¹

                    A measurable equivalence is a measurable embedding.

                    def MeasurableEquiv.cast {α β : Type u_6} [i₁ : MeasurableSpace α] [i₂ : MeasurableSpace β] (h : Eq α β) (hi : HEq i₁ i₂) :

                    Equal measurable spaces are equivalent.

                    Equations
                    Instances For

                      Measurable equivalence between ULift α and α.

                      Equations
                      Instances For
                        theorem MeasurableEquiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : βγ} (e : MeasurableEquiv α β) :

                        Any two types with unique elements are measurably equivalent.

                        Equations
                        Instances For
                          def MeasurableEquiv.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : MeasurableEquiv α β) (cd : MeasurableEquiv γ δ) :
                          MeasurableEquiv (Prod α γ) (Prod β δ)

                          Products of equivalent measurable spaces are equivalent.

                          Equations
                          Instances For
                            def MeasurableEquiv.prodComm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
                            MeasurableEquiv (Prod α β) (Prod β α)

                            Products of measurable spaces are symmetric.

                            Equations
                            Instances For
                              def MeasurableEquiv.prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                              MeasurableEquiv (Prod (Prod α β) γ) (Prod α (Prod β γ))

                              Products of measurable spaces are associative.

                              Equations
                              Instances For

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

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For
                                    def MeasurableEquiv.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : MeasurableEquiv α β) (cd : MeasurableEquiv γ δ) :
                                    MeasurableEquiv (Sum α γ) (Sum β δ)

                                    Sums of measurable spaces are symmetric.

                                    Equations
                                    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.

                                      Equations
                                      Instances For

                                        univ α ≃ α as measurable spaces.

                                        Equations
                                        Instances For

                                          {a} ≃ Unit as measurable spaces.

                                          Equations
                                          Instances For

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

                                            Equations
                                            Instances For

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

                                              Equations
                                              Instances For
                                                def MeasurableEquiv.sumProdDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                                                MeasurableEquiv (Prod (Sum α β) γ) (Sum (Prod α γ) (Prod β γ))

                                                Products distribute over sums (on the right) as measurable spaces.

                                                Equations
                                                Instances For
                                                  def MeasurableEquiv.prodSumDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                                                  MeasurableEquiv (Prod α (Sum β γ)) (Sum (Prod α β) (Prod α γ))

                                                  Products distribute over sums (on the left) as measurable spaces.

                                                  Equations
                                                  Instances For
                                                    def MeasurableEquiv.sumProdSum (α : Type u_6) (β : Type u_7) (γ : Type u_8) (δ : Type u_9) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] :
                                                    MeasurableEquiv (Prod (Sum α β) (Sum γ δ)) (Sum (Sum (Prod α γ) (Prod α δ)) (Sum (Prod β γ) (Prod β δ)))

                                                    Products distribute over sums as measurable spaces.

                                                    Equations
                                                    Instances For
                                                      def MeasurableEquiv.piCongrRight {δ' : Type u_5} {π : δ'Type u_6} {π' : δ'Type u_7} [(x : δ') → MeasurableSpace (π x)] [(x : δ') → MeasurableSpace (π' x)] (e : (a : δ') → MeasurableEquiv (π a) (π' a)) :
                                                      MeasurableEquiv ((a : δ') → π a) ((a : δ') → π' a)

                                                      A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence between Π a, β₁ a and Π a, β₂ a.

                                                      Equations
                                                      Instances For
                                                        def MeasurableEquiv.piCongrLeft {δ : Type u_4} {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (f : Equiv δ δ') :
                                                        MeasurableEquiv ((b : δ) → π (DFunLike.coe f b)) ((a : δ') → π a)

                                                        Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.

                                                        Equations
                                                        Instances For
                                                          theorem MeasurableEquiv.coe_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] (f : Equiv δ δ') :
                                                          theorem MeasurableEquiv.piCongrLeft_apply_apply {ι : Type u_8} {ι' : Type u_9} (e : Equiv ι ι') {β : ι'Type u_10} [(i' : ι') → MeasurableSpace (β i')] (x : (i : ι) → β (DFunLike.coe e i)) (i : ι) :
                                                          Eq (DFunLike.coe (piCongrLeft (fun (i' : ι') => β i') e) x (DFunLike.coe e i)) (x i)
                                                          def MeasurableEquiv.arrowProdEquivProdArrow (α : Type u_8) (β : Type u_9) (γ : Type u_10) [MeasurableSpace α] [MeasurableSpace β] :
                                                          MeasurableEquiv (γProd α β) (Prod (γα) (γβ))

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

                                                          Equations
                                                          Instances For
                                                            def MeasurableEquiv.arrowCongr' {α₁ : Type u_8} {β₁ : Type u_9} {α₂ : Type u_10} {β₂ : Type u_11} [MeasurableSpace β₁] [MeasurableSpace β₂] ( : Equiv α₁ α₂) ( : MeasurableEquiv β₁ β₂) :
                                                            MeasurableEquiv (α₁β₁) (α₂β₂)

                                                            The measurable equivalence (α₁ → β₁) ≃ᵐ (α₂ → β₂) induced by α₁ ≃ α₂ and β₁ ≃ᵐ β₂.

                                                            Equations
                                                            Instances For
                                                              def MeasurableEquiv.piMeasurableEquivTProd {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), Membership.mem l i) :
                                                              MeasurableEquiv ((i : δ') → π i) (List.TProd π l)

                                                              Pi-types are measurably equivalent to iterated products.

                                                              Equations
                                                              Instances For
                                                                theorem MeasurableEquiv.piMeasurableEquivTProd_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), Membership.mem l i) :
                                                                theorem MeasurableEquiv.piMeasurableEquivTProd_symm_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ (i : δ'), Membership.mem l i) :
                                                                def MeasurableEquiv.piUnique {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                                MeasurableEquiv ((i : δ') → π i) (π Inhabited.default)

                                                                The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆ when the domain of π only contains

                                                                Equations
                                                                Instances For
                                                                  theorem MeasurableEquiv.piUnique_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                                  Eq (DFunLike.coe (piUnique π)) fun (f : (i : δ') → π i) => f Inhabited.default
                                                                  theorem MeasurableEquiv.piUnique_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                                  def MeasurableEquiv.funUnique (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                                  MeasurableEquiv (αβ) β

                                                                  If α has a unique term, then the type of function α → β is measurably equivalent to β.

                                                                  Equations
                                                                  Instances For
                                                                    theorem MeasurableEquiv.funUnique_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                                    Eq (DFunLike.coe (funUnique α β)) fun (f : αβ) => f Inhabited.default
                                                                    def MeasurableEquiv.piFinTwo (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                    MeasurableEquiv ((i : Fin 2) → α i) (Prod (α 0) (α 1))

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

                                                                    Equations
                                                                    Instances For
                                                                      theorem MeasurableEquiv.piFinTwo_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                      Eq (DFunLike.coe (piFinTwo α)) fun (f : (i : Fin 2) → α i) => { fst := f 0, snd := f 1 }
                                                                      theorem MeasurableEquiv.piFinTwo_symm_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                      Eq (DFunLike.coe (piFinTwo α).symm) fun (p : Prod (α 0) (α 1)) => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

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

                                                                      Equations
                                                                      Instances For
                                                                        theorem MeasurableEquiv.finTwoArrow_apply {α : Type u_1} [MeasurableSpace α] :
                                                                        Eq (DFunLike.coe finTwoArrow) fun (f : Fin 2α) => { fst := f 0, snd := f 1 }
                                                                        def MeasurableEquiv.piFinSuccAbove {n : Nat} (α : Fin (HAdd.hAdd n 1)Type u_8) [(i : Fin (HAdd.hAdd n 1)) → MeasurableSpace (α i)] (i : Fin (HAdd.hAdd n 1)) :
                                                                        MeasurableEquiv ((j : Fin (HAdd.hAdd n 1)) → α j) (Prod (α 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
                                                                        Instances For
                                                                          def MeasurableEquiv.piEquivPiSubtypeProd {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                          MeasurableEquiv ((i : δ') → π i) (Prod ((i : Subtype p) → π i.val) ((i : Subtype fun (i : δ') => Not (p i)) → π i.val))

                                                                          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
                                                                          Instances For
                                                                            theorem MeasurableEquiv.piEquivPiSubtypeProd_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                            Eq (DFunLike.coe (piEquivPiSubtypeProd π p)) fun (f : (i : δ') → π i) => { fst := fun (x : Subtype fun (x : δ') => p x) => f x.val, snd := fun (x : Subtype fun (x : δ') => Not (p x)) => f x.val }
                                                                            theorem MeasurableEquiv.piEquivPiSubtypeProd_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                            Eq (DFunLike.coe (piEquivPiSubtypeProd π p).symm) fun (f : Prod ((i : Subtype fun (x : δ') => p x) → π i.val) ((i : Subtype fun (x : δ') => Not (p x)) → π i.val)) (x : δ') => if h : p x then f.fst x, h else f.snd x, h
                                                                            def MeasurableEquiv.sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : Sum δ δ'Type u_8) [(i : Sum δ δ') → MeasurableSpace (α i)] :
                                                                            MeasurableEquiv ((i : Sum δ δ') → α i) (Prod ((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
                                                                            Instances For
                                                                              theorem MeasurableEquiv.coe_sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : Sum δ δ'Type u_8) [(i : Sum δ δ') → MeasurableSpace (α i)] :
                                                                              theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm {δ : Type u_4} {δ' : Type u_5} (α : Sum δ δ'Type u_8) [(i : Sum δ δ') → MeasurableSpace (α i)] :
                                                                              def MeasurableEquiv.piOptionEquivProd {δ : Type u_8} (α : Option δType u_9) [(i : Option δ) → MeasurableSpace (α i)] :
                                                                              MeasurableEquiv ((i : Option δ) → α i) (Prod ((i : δ) → α (Option.some i)) (α Option.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
                                                                                def MeasurableEquiv.piFinsetUnion {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {s t : Finset δ'} (h : Disjoint s t) :
                                                                                MeasurableEquiv (Prod ((i : Subtype fun (x : δ') => Membership.mem s x) → π i.val) ((i : Subtype fun (x : δ') => Membership.mem t x) → π i.val)) ((i : Subtype fun (x : δ') => Membership.mem (Union.union s t) x) → π i.val)

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

                                                                                    Equations
                                                                                    Instances For
                                                                                      theorem MeasurableEquiv.ofInvolutive_apply {α : Type u_1} [MeasurableSpace α] (f : αα) (hf : Function.Involutive f) (hf' : Measurable f) (a : α) :
                                                                                      Eq (DFunLike.coe (ofInvolutive f hf hf') a) (f a)
                                                                                      theorem MeasurableEquiv.ofInvolutive_symm {α : Type u_1} [MeasurableSpace α] (f : αα) (hf : Function.Involutive f) (hf' : Measurable f) :
                                                                                      Eq (ofInvolutive f hf hf').symm (ofInvolutive f hf hf')
                                                                                      theorem MeasurableEmbedding.comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
                                                                                      Eq (MeasurableSpace.comap f inst✝) inst✝¹
                                                                                      theorem MeasurableEmbedding.iff_comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} :
                                                                                      noncomputable def MeasurableEmbedding.equivImage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (s : Set α) (hf : MeasurableEmbedding f) :

                                                                                      A set is equivalent to its image under a function f as measurable spaces, if f is a measurable embedding

                                                                                      Equations
                                                                                      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

                                                                                        Equations
                                                                                        Instances For
                                                                                          theorem MeasurableEmbedding.of_measurable_inverse {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {g : βα} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g f) :
                                                                                          noncomputable def MeasurableEmbedding.schroederBernstein {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {g : βα} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g) :

                                                                                          The measurable Schröder-Bernstein Theorem: given measurable embeddings α → β and β → α, we can find a measurable equivalence α ≃ᵐ β.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For