Documentation

Mathlib.MeasureTheory.MeasurableSpace.Basic

Measurable spaces and measurable functions #

This file provides properties of measurable spaces and the functions and isomorphisms between them. The definition of a measurable space is in Mathlib/MeasureTheory/MeasurableSpace/Defs.lean.

A measurable space is a set equipped with a σ-algebra, a collection of subsets closed under complementation and countable union. A function between measurable spaces is measurable if the preimage of each measurable subset is measurable.

σ-algebras on a fixed set α form a complete lattice. Here we order σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any collection of subsets of α generates a smallest σ-algebra which contains all of them. A function f : α → β induces a Galois connection between the lattices of σ-algebras on α and β.

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.

We say that a filter f is measurably generated if every set s ∈ f includes a measurable set t ∈ f. This property is useful, e.g., to extract a measurable witness of Filter.Eventually.

Notation #

Implementation notes #

Measurability of a function f : α → β between measurable spaces is defined in terms of the Galois connection induced by f.

References #

Tags #

measurable space, σ-algebra, measurable function, measurable equivalence, dynkin system, π-λ theorem, π-system

def MeasurableSpace.map {α : Type u_1} {β : Type u_2} (f : αβ) (m : MeasurableSpace α) :

The forward image of a measurable space under a function. map f m contains the sets s : Set β whose preimage under f is measurable.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem MeasurableSpace.map_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : αβ} {s : Set β} :
    @[simp]
    @[simp]
    theorem MeasurableSpace.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : αβ} {g : βγ} :
    def MeasurableSpace.comap {α : Type u_1} {β : Type u_2} (f : αβ) (m : MeasurableSpace β) :

    The reverse image of a measurable space under a function. comap f m contains the sets s : Set α such that s is the f-preimage of a measurable set in β.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem MeasurableSpace.comap_eq_generateFrom {α : Type u_1} {β : Type u_2} (m : MeasurableSpace β) (f : αβ) :
      @[simp]
      @[simp]
      theorem MeasurableSpace.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : βα} {g : γβ} :
      theorem MeasurableSpace.comap_le_iff_le_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m' : MeasurableSpace β} {f : αβ} :
      theorem MeasurableSpace.map_mono {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {f : αβ} (h : m₁ m₂) :
      theorem MeasurableSpace.monotone_map {α : Type u_1} {β : Type u_2} {f : αβ} :
      theorem MeasurableSpace.comap_mono {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {g : βα} (h : m₁ m₂) :
      theorem MeasurableSpace.monotone_comap {α : Type u_1} {β : Type u_2} {g : βα} :
      @[simp]
      theorem MeasurableSpace.comap_bot {α : Type u_1} {β : Type u_2} {g : βα} :
      @[simp]
      theorem MeasurableSpace.comap_sup {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {g : βα} :
      @[simp]
      theorem MeasurableSpace.comap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort uι} {g : βα} {m : ιMeasurableSpace α} :
      MeasurableSpace.comap g (⨆ (i : ι), m i) = ⨆ (i : ι), MeasurableSpace.comap g (m i)
      @[simp]
      theorem MeasurableSpace.map_top {α : Type u_1} {β : Type u_2} {f : αβ} :
      @[simp]
      theorem MeasurableSpace.map_inf {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {f : αβ} :
      @[simp]
      theorem MeasurableSpace.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort uι} {f : αβ} {m : ιMeasurableSpace α} :
      MeasurableSpace.map f (⨅ (i : ι), m i) = ⨅ (i : ι), MeasurableSpace.map f (m i)
      theorem MeasurableSpace.comap_map_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : αβ} :
      theorem MeasurableSpace.le_map_comap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : βα} :
      @[simp]
      theorem MeasurableSpace.map_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} (b : β) :
      MeasurableSpace.map (fun (_a : α) => b) m =
      @[simp]
      theorem MeasurableSpace.comap_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (b : β) :
      MeasurableSpace.comap (fun (_a : α) => b) m =
      theorem measurable_iff_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :
      theorem Measurable.le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :

      Alias of the forward direction of measurable_iff_le_map.

      theorem Measurable.of_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :

      Alias of the reverse direction of measurable_iff_le_map.

      theorem measurable_iff_comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :
      theorem Measurable.of_comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :

      Alias of the reverse direction of measurable_iff_comap_le.

      theorem Measurable.comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :

      Alias of the forward direction of measurable_iff_comap_le.

      theorem comap_measurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (f : αβ) :
      theorem Measurable.mono {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {ma' : MeasurableSpace α} {mb : MeasurableSpace β} {mb' : MeasurableSpace β} {f : αβ} (hf : Measurable f) (ha : ma ma') (hb : mb' mb) :
      theorem measurable_id'' {α : Type u_1} {m : MeasurableSpace α} {mα : MeasurableSpace α} (hm : m ) :
      theorem measurable_from_top {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {f : αβ} :
      theorem measurable_generateFrom {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set (Set β)} {f : αβ} (h : ts, MeasurableSet (f ⁻¹' t)) :
      theorem Subsingleton.measurable {α : Type u_1} {β : Type u_2} {f : αβ} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton α] :
      theorem measurable_of_subsingleton_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton β] (f : αβ) :
      theorem measurable_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Zero α] :
      theorem measurable_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [One α] :
      theorem measurable_of_empty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty α] (f : αβ) :
      theorem measurable_of_empty_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty β] (f : αβ) :
      theorem measurable_const' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : βα} (hf : ∀ (x y : β), f x = f y) :

      A version of measurable_const that assumes f x = f y for all x, y. This version works for functions between empty types.

      theorem measurable_natCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [NatCast α] (n : ) :
      theorem measurable_intCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IntCast α] (n : ) :
      theorem measurable_of_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (f : αβ) :
      theorem measurable_of_finite {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Finite α] [MeasurableSingletonClass α] (f : αβ) :
      theorem Measurable.iterate {α : Type u_1} {m : MeasurableSpace α} {f : αα} (hf : Measurable f) (n : ) :
      theorem measurableSet_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (hf : Measurable f) (ht : MeasurableSet t) :
      theorem MeasurableSet.preimage {α : Type u_1} {β : Type u_2} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (ht : MeasurableSet t) (hf : Measurable f) :
      theorem Measurable.piecewise {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {g : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
      ∀ {x : DecidablePred fun (x : α) => x s}, MeasurableSet sMeasurable fMeasurable gMeasurable (Set.piecewise s f g)
      theorem Measurable.ite {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : αProp} :
      ∀ {x : DecidablePred p}, MeasurableSet {a : α | p a}Measurable fMeasurable gMeasurable fun (x_1 : α) => if p x_1 then f x_1 else g x_1

      This is slightly different from Measurable.piecewise. It can be used to show Measurable (ite (x=0) 0 1) by exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const, but replacing Measurable.ite by Measurable.piecewise in that example proof does not work.

      theorem Measurable.indicator {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] (hf : Measurable f) (hs : MeasurableSet s) :
      theorem measurable_indicator_const_iff {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (b : β) [NeZero b] :
      Measurable (Set.indicator s fun (x : α) => b) MeasurableSet s

      The measurability of a set A is equivalent to the measurability of the indicator function which takes a constant value b ≠ 0 on a set A and 0 elsewhere.

      theorem measurableSet_support {α : Type u_1} {β : Type u_2} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (hf : Measurable f) :
      theorem measurableSet_mulSupport {α : Type u_1} {β : Type u_2} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [One β] [MeasurableSingletonClass β] (hf : Measurable f) :
      theorem Measurable.measurable_of_countable_ne {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] (hf : Measurable f) (h : Set.Countable {x : α | f x g x}) :

      If a function coincides with a measurable function outside of a countable set, it is measurable.

      theorem measurable_to_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : βα} (h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})) :
      theorem measurable_to_countable' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : βα} (h : ∀ (x : α), MeasurableSet (f ⁻¹' {x})) :
      theorem measurable_unit {α : Type u_1} [MeasurableSpace α] (f : Unitα) :
      Equations
      theorem measurable_down {α : Type u_1} [MeasurableSpace α] :
      Measurable ULift.down
      theorem measurable_up {α : Type u_1} [MeasurableSpace α] :
      Measurable ULift.up
      @[simp]
      theorem measurableSet_preimage_down {α : Type u_1} [MeasurableSpace α] {s : Set α} :
      theorem measurable_from_nat {α : Type u_1} [MeasurableSpace α] {f : α} :
      theorem measurable_to_nat {α : Type u_1} [MeasurableSpace α] {f : α} :
      (∀ (y : α), MeasurableSet (f ⁻¹' {f y}))Measurable f
      theorem measurable_to_bool {α : Type u_1} [MeasurableSpace α] {f : αBool} (h : MeasurableSet (f ⁻¹' {true})) :
      theorem measurable_to_prop {α : Type u_1} [MeasurableSpace α] {f : αProp} (h : MeasurableSet (f ⁻¹' {True})) :
      theorem measurable_findGreatest' {α : Type u_1} [MeasurableSpace α] {p : αProp} [(x : α) → DecidablePred (p x)] {N : } (hN : kN, MeasurableSet {x : α | Nat.findGreatest (p x) N = k}) :
      Measurable fun (x : α) => Nat.findGreatest (p x) N
      theorem measurable_findGreatest {α : Type u_1} [MeasurableSpace α] {p : αProp} [(x : α) → DecidablePred (p x)] {N : } (hN : kN, MeasurableSet {x : α | p x k}) :
      Measurable fun (x : α) => Nat.findGreatest (p x) N
      theorem measurable_find {α : Type u_1} [MeasurableSpace α] {p : αProp} [(x : α) → DecidablePred (p x)] (hp : ∀ (x : α), ∃ (N : ), p x N) (hm : ∀ (k : ), MeasurableSet {x : α | p x k}) :
      Measurable fun (x : α) => Nat.find (_ : ∃ (N : ), p x N)
      instance Quot.instMeasurableSpace {α : Type u_6} {r : ααProp} [m : MeasurableSpace α] :
      Equations
      Equations
      Equations
      Equations
      theorem measurableSet_quotient {α : Type u_1} [MeasurableSpace α] {s : Setoid α} {t : Set (Quotient s)} :
      theorem measurable_from_quotient {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {s : Setoid α} {f : Quotient sβ} :
      Measurable f Measurable (f Quotient.mk'')
      theorem measurable_quotient_mk' {α : Type u_1} [MeasurableSpace α] [s : Setoid α] :
      Measurable Quotient.mk'
      theorem measurable_quotient_mk'' {α : Type u_1} [MeasurableSpace α] {s : Setoid α} :
      Measurable Quotient.mk''
      theorem measurable_quot_mk {α : Type u_1} [MeasurableSpace α] {r : ααProp} :
      theorem QuotientAddGroup.measurable_coe {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} :
      Measurable QuotientAddGroup.mk
      theorem QuotientGroup.measurable_coe {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} :
      Measurable QuotientGroup.mk
      theorem QuotientAddGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} {f : G Sα} :
      Measurable f Measurable (f QuotientAddGroup.mk)
      theorem QuotientGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} {f : G Sα} :
      Measurable f Measurable (f QuotientGroup.mk)
      instance Subtype.instMeasurableSpace {α : Type u_6} {p : αProp} [m : MeasurableSpace α] :
      Equations
      theorem measurable_subtype_coe {α : Type u_1} [MeasurableSpace α] {p : αProp} :
      Measurable Subtype.val
      theorem MeasurableSet.of_subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set s} (h : MeasurableSet (Subtype.val '' t)) :
      theorem MeasurableSet.subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set s} (hs : MeasurableSet s) :
      MeasurableSet tMeasurableSet (Subtype.val '' t)
      theorem Measurable.subtype_coe {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : βProp} {f : αSubtype p} (hf : Measurable f) :
      Measurable fun (a : α) => (f a)
      theorem Measurable.subtype_val {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : βProp} {f : αSubtype p} (hf : Measurable f) :
      Measurable fun (a : α) => (f a)

      Alias of Measurable.subtype_coe.

      theorem Measurable.subtype_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : βProp} {f : αβ} (hf : Measurable f) {h : ∀ (x : α), p (f x)} :
      Measurable fun (x : α) => { val := f x, property := (_ : p (f x)) }
      theorem Measurable.rangeFactorization {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} (hf : Measurable f) :
      theorem Measurable.subtype_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} {p : αProp} {q : βProp} (hf : Measurable f) (hpq : ∀ (x : α), p xq (f x)) :
      theorem measurable_inclusion {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s t) :
      theorem MeasurableSet.image_inclusion' {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s t) {u : Set s} (hs : MeasurableSet (Subtype.val ⁻¹' s)) (hu : MeasurableSet u) :
      theorem MeasurableSet.image_inclusion {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s t) {u : Set s} (hs : MeasurableSet s) (hu : MeasurableSet u) :
      theorem MeasurableSet.of_union_cover {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} {u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ s t) (hsu : MeasurableSet (Subtype.val ⁻¹' u)) (htu : MeasurableSet (Subtype.val ⁻¹' u)) :
      theorem measurable_of_measurable_union_cover {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} (s : Set α) (t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ s t) (hc : Measurable fun (a : s) => f a) (hd : Measurable fun (a : t) => f a) :
      theorem measurable_of_restrict_of_restrict_compl {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} {s : Set α} (hs : MeasurableSet s) (h₁ : Measurable (Set.restrict s f)) (h₂ : Measurable (Set.restrict s f)) :
      theorem Measurable.dite {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [(x : α) → Decidable (x s)] {f : sβ} (hf : Measurable f) {g : sβ} (hg : Measurable g) (hs : MeasurableSet s) :
      Measurable fun (x : α) => if hx : x s then f { val := x, property := hx } else g { val := x, property := hx }
      theorem measurable_of_measurable_on_compl_finite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {f : αβ} (s : Set α) (hs : Set.Finite s) (hf : Measurable (Set.restrict s f)) :
      theorem measurable_of_measurable_on_compl_singleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {f : αβ} (a : α) (hf : Measurable (Set.restrict {x : α | x a} f)) :
      def MeasurableSpace.prod {α : Type u_6} {β : Type u_7} (m₁ : MeasurableSpace α) (m₂ : MeasurableSpace β) :

      A MeasurableSpace structure on the product of two measurable spaces.

      Equations
      Instances For
        instance Prod.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :
        Equations
        theorem measurable_fst {α : Type u_1} {β : Type u_2} :
        ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst
        theorem measurable_snd {α : Type u_1} {β : Type u_2} :
        ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.snd
        theorem Measurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} (hf : Measurable f) :
        Measurable fun (a : α) => (f a).1
        theorem Measurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} (hf : Measurable f) :
        Measurable fun (a : α) => (f a).2
        theorem Measurable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} (hf₁ : Measurable fun (a : α) => (f a).1) (hf₂ : Measurable fun (a : α) => (f a).2) :
        theorem Measurable.prod_mk {α : Type u_1} {m : MeasurableSpace α} {β : Type u_6} {γ : Type u_7} :
        ∀ {x : MeasurableSpace β} {x_1 : MeasurableSpace γ} {f : αβ} {g : αγ}, Measurable fMeasurable gMeasurable fun (a : α) => (f a, g a)
        theorem Measurable.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace δ] {f : αβ} {g : γδ} (hf : Measurable f) (hg : Measurable g) :
        theorem measurable_prod_mk_left {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α} :
        theorem measurable_prod_mk_right {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {y : β} :
        Measurable fun (x : α) => (x, y)
        theorem Measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβγ} (hf : Measurable (Function.uncurry f)) {x : α} :
        theorem Measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβγ} (hf : Measurable (Function.uncurry f)) {y : β} :
        Measurable fun (x : α) => f x y
        theorem measurable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} :
        Measurable f (Measurable fun (a : α) => (f a).1) Measurable fun (a : α) => (f a).2
        theorem measurable_swap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
        Measurable Prod.swap
        theorem measurable_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
        ∀ {x : MeasurableSpace γ} {f : α × βγ}, Measurable (f Prod.swap) Measurable f
        theorem MeasurableSet.prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) :
        theorem measurableSet_prod_of_nonempty {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (h : Set.Nonempty (s ×ˢ t)) :
        theorem measurableSet_prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} :
        theorem measurableSet_swap_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α × β)} :
        theorem measurable_from_prod_countable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable β] [MeasurableSingletonClass β] :
        ∀ {x : MeasurableSpace γ} {f : α × βγ}, (∀ (y : β), Measurable fun (x : α) => f (x, y))Measurable f
        theorem Measurable.find {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} :
        ∀ {x : MeasurableSpace α} {f : αβ} {p : αProp} [inst : (n : ) → DecidablePred (p n)], (∀ (n : ), Measurable (f n))(∀ (n : ), MeasurableSet {x : α | p n x})∀ (h : ∀ (x : α), ∃ (n : ), p n x), Measurable fun (x : α) => f (Nat.find (_ : ∃ (n : ), p n x)) x

        A piecewise function on countably many pieces is measurable if all the data is measurable.

        theorem measurable_iUnionLift {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] {t : ιSet α} {f : (i : ι) → (t i)β} (htf : ∀ (i j : ι) (x : α) (hxi : x t i) (hxj : x t j), f i { val := x, property := hxi } = f j { val := x, property := hxj }) {T : Set α} (hT : T ⋃ (i : ι), t i) (htm : ∀ (i : ι), MeasurableSet (t i)) (hfm : ∀ (i : ι), Measurable (f i)) :
        Measurable (Set.iUnionLift t f htf T hT)

        Let t i be a countable covering of a set T by measurable sets. Let f i : t i → β be a family of functions that agree on the intersections t i ∩ t j. Then the function Set.iUnionLift t f _ _ : T → β, defined as f i ⟨x, hx⟩ for hx : x ∈ t i, is measurable.

        theorem measurable_liftCover {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (t : ιSet α) (htm : ∀ (i : ι), MeasurableSet (t i)) (f : (i : ι) → (t i)β) (hfm : ∀ (i : ι), Measurable (f i)) (hf : ∀ (i j : ι) (x : α) (hxi : x t i) (hxj : x t j), f i { val := x, property := hxi } = f j { val := x, property := hxj }) (htU : ⋃ (i : ι), t i = Set.univ) :

        Let t i be a countable covering of α by measurable sets. Let f i : t i → β be a family of functions that agree on the intersections t i ∩ t j. Then the function Set.liftCover t f _ _, defined as f i ⟨x, hx⟩ for hx : x ∈ t i, is measurable.

        theorem exists_measurable_piecewise {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {ι : Type u_6} [Countable ι] [Nonempty ι] (t : ιSet α) (t_meas : ∀ (n : ι), MeasurableSet (t n)) (g : ιαβ) (hg : ∀ (n : ι), Measurable (g n)) (ht : Pairwise fun (i j : ι) => Set.EqOn (g i) (g j) (t i t j)) :
        ∃ (f : αβ), Measurable f ∀ (n : ι), Set.EqOn f (g n) (t n)

        Let t i be a nonempty countable family of measurable sets in α. Let g i : α → β be a family of measurable functions such that g i agrees with g j on t i ∩ t j. Then there exists a measurable function f : α → β that agrees with each g i on t i.

        We only need the assumption [Nonempty ι] to prove [Nonempty (α → β)].

        @[deprecated exists_measurable_piecewise]
        theorem exists_measurable_piecewise_nat {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m : MeasurableSpace α} (t : Set β) (t_meas : ∀ (n : ), MeasurableSet (t n)) (t_disj : Pairwise (Disjoint on t)) (g : βα) (hg : ∀ (n : ), Measurable (g n)) :
        ∃ (f : βα), Measurable f ∀ (n : ), xt n, f x = g n x

        Given countably many disjoint measurable sets t n and countably many measurable functions g n, one can construct a measurable function that coincides with g n on t n.

        instance MeasurableSpace.pi {δ : Type u_4} {π : δType u_6} [m : (a : δ) → MeasurableSpace (π a)] :
        MeasurableSpace ((a : δ) → π a)
        Equations
        theorem measurable_pi_iff {α : Type u_1} {δ : Type u_4} {π : δType u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] {g : α(a : δ) → π a} :
        Measurable g ∀ (a : δ), Measurable fun (x : α) => g x a
        theorem measurable_pi_apply {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] (a : δ) :
        Measurable fun (f : (a : δ) → π a) => f a
        theorem Measurable.eval {α : Type u_1} {δ : Type u_4} {π : δType u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] {a : δ} {g : α(a : δ) → π a} (hg : Measurable g) :
        Measurable fun (x : α) => g x a
        theorem measurable_pi_lambda {α : Type u_1} {δ : Type u_4} {π : δType u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] (f : α(a : δ) → π a) (hf : ∀ (a : δ), Measurable fun (c : α) => f c a) :
        theorem measurable_update' {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {a : δ} [DecidableEq δ] :
        Measurable fun (p : ((i : δ) → π i) × π a) => Function.update p.1 a p.2

        The function (f, x) ↦ update f a x : (Π a, π a) × π a → Π a, π a is measurable.

        theorem measurable_uniqueElim {δ : Type u_4} {π : δType u_6} [Unique δ] [(i : δ) → MeasurableSpace (π i)] :
        Measurable uniqueElim
        theorem measurable_updateFinset {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [DecidableEq δ] {s : Finset δ} {x : (i : δ) → π i} :
        theorem measurable_update {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] (f : (a : δ) → π a) {a : δ} [DecidableEq δ] :

        The function update f a : π a → Π a, π a is always measurable. This doesn't require f to be measurable. This should not be confused with the statement that update f a x is measurable.

        theorem measurable_update_left {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {a : δ} [DecidableEq δ] {x : π a} :
        Measurable fun (x_1 : (a : δ) → π a) => Function.update x_1 a x
        theorem measurable_eq_mp {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] {i : δ} {i' : δ} (h : i = i') :
        Measurable (Eq.mp (_ : π i = π i'))
        theorem Measurable.eq_mp {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] {β : Type u_7} [MeasurableSpace β] {i : δ} {i' : δ} (h : i = i') {f : βπ i} (hf : Measurable f) :
        Measurable fun (x : β) => Eq.mp (_ : π i = π i') (f x)
        theorem measurable_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] (f : δ' δ) :
        theorem MeasurableSet.pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : Set.Countable s) (ht : is, MeasurableSet (t i)) :
        theorem MeasurableSet.univ_pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [Countable δ] {t : (i : δ) → Set (π i)} (ht : ∀ (i : δ), MeasurableSet (t i)) :
        MeasurableSet (Set.pi Set.univ t)
        theorem measurableSet_pi_of_nonempty {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : Set.Countable s) (h : Set.Nonempty (Set.pi s t)) :
        MeasurableSet (Set.pi s t) is, MeasurableSet (t i)
        theorem measurableSet_pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : Set.Countable s) :
        MeasurableSet (Set.pi s t) (is, MeasurableSet (t i)) Set.pi s t =
        instance Pi.instMeasurableSingletonClass {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [Countable δ] [∀ (a : δ), MeasurableSingletonClass (π a)] :
        MeasurableSingletonClass ((a : δ) → π a)
        Equations
        theorem measurable_piEquivPiSubtypeProd_symm {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] (p : δProp) [DecidablePred p] :
        theorem measurable_piEquivPiSubtypeProd {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] (p : δProp) [DecidablePred p] :
        instance TProd.instMeasurableSpace {δ : Type u_4} (π : δType u_6) [(x : δ) → MeasurableSpace (π x)] (l : List δ) :
        Equations
        theorem measurable_tProd_mk {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] (l : List δ) :
        theorem measurable_tProd_elim {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] [DecidableEq δ] {l : List δ} {i : δ} (hi : i l) :
        Measurable fun (v : List.TProd π l) => List.TProd.elim v hi
        theorem measurable_tProd_elim' {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] [DecidableEq δ] {l : List δ} (h : ∀ (i : δ), i l) :
        theorem MeasurableSet.tProd {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] (l : List δ) {s : (i : δ) → Set (π i)} (hs : ∀ (i : δ), MeasurableSet (s i)) :
        instance Sum.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :
        Equations
        theorem measurable_inl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
        Measurable Sum.inl
        theorem measurable_inr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
        Measurable Sum.inr
        theorem measurableSet_sum_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α β)} :
        theorem measurable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
        ∀ {x : MeasurableSpace γ} {f : α βγ}, Measurable (f Sum.inl)Measurable (f Sum.inr)Measurable f
        theorem Measurable.sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
        ∀ {x : MeasurableSpace γ} {f : αγ} {g : βγ}, Measurable fMeasurable gMeasurable (Sum.elim f g)
        theorem Measurable.sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
        ∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace δ} {f : αβ} {g : γδ}, Measurable fMeasurable gMeasurable (Sum.map f g)
        @[simp]
        theorem measurableSet_inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :
        theorem MeasurableSet.inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :
        MeasurableSet sMeasurableSet (Sum.inl '' s)

        Alias of the reverse direction of measurableSet_inl_image.

        @[simp]
        theorem measurableSet_inr_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} :
        theorem MeasurableSet.inr_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} :
        MeasurableSet sMeasurableSet (Sum.inr '' s)

        Alias of the reverse direction of measurableSet_inr_image.

        theorem measurableSet_range_inl {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace α] :
        theorem measurableSet_range_inr {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace α] :
        instance Sigma.instMeasurableSpace {α : Type u_7} {β : αType u_6} [m : (a : α) → MeasurableSpace (β a)] :
        Equations
        @[simp]
        theorem measurableSet_setOf {α : Type u_1} [MeasurableSpace α] {p : αProp} :
        MeasurableSet {a : α | p a} Measurable p
        @[simp]
        theorem measurable_mem {α : Type u_1} {s : Set α} [MeasurableSpace α] :
        (Measurable fun (x : α) => x s) MeasurableSet s
        theorem Measurable.setOf {α : Type u_1} [MeasurableSpace α] {p : αProp} :
        Measurable pMeasurableSet {a : α | p a}

        Alias of the reverse direction of measurableSet_setOf.

        theorem MeasurableSet.mem {α : Type u_1} {s : Set α} [MeasurableSpace α] :
        MeasurableSet sMeasurable fun (x : α) => x s

        Alias of the reverse direction of measurable_mem.

        theorem Measurable.not {α : Type u_1} [MeasurableSpace α] {p : αProp} (hp : Measurable p) :
        Measurable fun (x : α) => ¬p x
        theorem Measurable.and {α : Type u_1} [MeasurableSpace α] {p : αProp} {q : αProp} (hp : Measurable p) (hq : Measurable q) :
        Measurable fun (a : α) => p a q a
        theorem Measurable.or {α : Type u_1} [MeasurableSpace α] {p : αProp} {q : αProp} (hp : Measurable p) (hq : Measurable q) :
        Measurable fun (a : α) => p a q a
        theorem Measurable.imp {α : Type u_1} [MeasurableSpace α] {p : αProp} {q : αProp} (hp : Measurable p) (hq : Measurable q) :
        Measurable fun (a : α) => p aq a
        theorem Measurable.iff {α : Type u_1} [MeasurableSpace α] {p : αProp} {q : αProp} (hp : Measurable p) (hq : Measurable q) :
        Measurable fun (a : α) => p a q a
        theorem Measurable.forall {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] [Countable ι] {p : ιαProp} (hp : ∀ (i : ι), Measurable (p i)) :
        Measurable fun (a : α) => ∀ (i : ι), p i a
        theorem Measurable.exists {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] [Countable ι] {p : ιαProp} (hp : ∀ (i : ι), Measurable (p i)) :
        Measurable fun (a : α) => ∃ (i : ι), p i a

        This instance is useful when talking about Bernoulli sequences of random variables or binomial random graphs.

        Equations
        • Set.instMeasurableSpace = id inferInstance
        theorem measurable_set_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {g : βSet α} :
        Measurable g ∀ (a : α), Measurable fun (x : β) => a g x
        theorem measurable_set_mem {α : Type u_1} (a : α) :
        Measurable fun (s : Set α) => a s
        theorem measurable_set_not_mem {α : Type u_1} (a : α) :
        Measurable fun (s : Set α) => as
        theorem measurableSet_mem {α : Type u_1} (a : α) :
        MeasurableSet {s : Set α | a s}
        theorem measurableSet_not_mem {α : Type u_1} (a : α) :
        MeasurableSet {s : Set α | as}
        theorem measurable_compl {α : Type u_1} :
        Measurable fun (x : Set α) => x
        @[simp]

        The sigma-algebra generated by a single set s is {∅, s, sᶜ, univ}.

        structure MeasurableEmbedding {α : Type u_6} {β : Type u_7} [MeasurableSpace α] [MeasurableSpace β] (f : αβ) :

        A map f : α → β is called a measurable embedding if it is injective, measurable, and sends measurable sets to measurable sets. The latter assumption can be replaced with “f has measurable inverse g : Set.range f → α”, see MeasurableEmbedding.measurable_rangeSplitting, MeasurableEmbedding.of_measurable_inverse_range, and MeasurableEmbedding.of_measurable_inverse.

        One more interpretation: f is a measurable embedding if it defines a measurable equivalence to its range and the range is a measurable set. One implication is formalized as MeasurableEmbedding.equivRange; the other one follows from MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.subtype_coe, and MeasurableEmbedding.comp.

        • injective : Function.Injective f

          A measurable embedding is injective.

        • measurable : Measurable f

          A measurable embedding is a measurable function.

        • measurableSet_image' : ∀ ⦃s : Set α⦄, MeasurableSet sMeasurableSet (f '' s)

          The image of a measurable set under a measurable embedding is a measurable set.

        Instances For
          theorem MeasurableEmbedding.measurableSet_image {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) {s : Set α} :
          theorem MeasurableEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {g : βγ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
          theorem MeasurableEmbedding.subtype_coe {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) :
          theorem MeasurableEmbedding.measurableSet_range {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
          theorem MeasurableEmbedding.measurableSet_preimage {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) {s : Set β} :
          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') :
          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 : βNonempty γ) :
          ∃ (g' : βγ), Measurable g' g' f = g
          theorem MeasurableEmbedding.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : αβ} {g : βγ} (hg : MeasurableEmbedding g) :
          theorem MeasurableSet.exists_measurable_proj {α : Type u_1} :
          ∀ {x : MeasurableSpace α} {s : Set α}, MeasurableSet sSet.Nonempty s∃ (f : αs), Measurable f ∀ (x : s), f x = 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.

          • 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
            Instances For
              theorem MeasurableEquiv.toEquiv_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
              Function.Injective MeasurableEquiv.toEquiv
              instance MeasurableEquiv.instEquivLike {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
              EquivLike (α ≃ᵐ β) α β
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem MeasurableEquiv.coe_toEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
              e.toEquiv = e
              theorem MeasurableEquiv.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
              @[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
              def MeasurableEquiv.refl (α : Type u_6) [MeasurableSpace α] :
              α ≃ᵐ α

              Any measurable space is equivalent to itself.

              Equations
              Instances For
                Equations
                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
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem MeasurableEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
                  (ab.trans bc) = bc ab
                  def MeasurableEquiv.symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (ab : α ≃ᵐ β) :
                  β ≃ᵐ α

                  The inverse of an equivalence between measurable spaces.

                  Equations
                  • ab.symm = { toEquiv := ab.symm, measurable_toFun := (_ : Measurable ab.symm), measurable_invFun := (_ : Measurable ab.toEquiv) }
                  Instances For
                    @[simp]
                    theorem MeasurableEquiv.coe_toEquiv_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                    e.symm = e.symm
                    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
                    Instances For
                      def MeasurableEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : α ≃ᵐ β) :
                      βα

                      See Note [custom simps projection]

                      Equations
                      Instances For
                        theorem MeasurableEquiv.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ : α ≃ᵐ β} {e₂ : α ≃ᵐ β} (h : e₁ = e₂) :
                        e₁ = e₂
                        @[simp]
                        theorem MeasurableEquiv.symm_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α β) (h1 : Measurable e) (h2 : Measurable e.symm) :
                        { toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm = { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }
                        @[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
                        @[simp]
                        theorem MeasurableEquiv.refl_apply (α : Type u_6) [MeasurableSpace α] (a : α) :
                        @[simp]
                        theorem MeasurableEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
                        ∀ (a : α), (ab.trans bc) a = bc (ab a)
                        @[simp]
                        theorem MeasurableEquiv.symm_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        e.symm.symm = e
                        theorem MeasurableEquiv.symm_bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
                        Function.Bijective MeasurableEquiv.symm
                        @[simp]
                        theorem MeasurableEquiv.symm_comp_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        e.symm e = id
                        @[simp]
                        theorem MeasurableEquiv.self_comp_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        e e.symm = id
                        @[simp]
                        theorem MeasurableEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (y : β) :
                        e (e.symm y) = y
                        @[simp]
                        theorem MeasurableEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (x : α) :
                        e.symm (e x) = x
                        @[simp]
                        theorem MeasurableEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        e.symm.trans e = MeasurableEquiv.refl β
                        @[simp]
                        theorem MeasurableEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        e.trans e.symm = MeasurableEquiv.refl α
                        theorem MeasurableEquiv.surjective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        theorem MeasurableEquiv.bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        theorem MeasurableEquiv.injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        @[simp]
                        theorem MeasurableEquiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
                        e.symm ⁻¹' (e ⁻¹' s) = s
                        theorem MeasurableEquiv.image_eq_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
                        e '' s = e.symm ⁻¹' s
                        theorem MeasurableEquiv.preimage_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
                        e.symm ⁻¹' s = e '' s
                        theorem MeasurableEquiv.image_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
                        e.symm '' s = e ⁻¹' s
                        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
                        @[simp]
                        theorem MeasurableEquiv.image_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :
                        e '' (e ⁻¹' s) = s
                        @[simp]
                        theorem MeasurableEquiv.preimage_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :
                        e ⁻¹' (e '' s) = s
                        @[simp]
                        theorem MeasurableEquiv.measurableSet_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) {s : Set β} :
                        @[simp]
                        theorem MeasurableEquiv.measurableSet_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) {s : Set α} :
                        @[simp]
                        theorem MeasurableEquiv.map_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :
                        MeasurableSpace.map (e) inst✝¹ = inst✝

                        A measurable equivalence is a measurable embedding.

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

                        Equal measurable spaces are equivalent.

                        Equations
                        Instances For

                          Measurable equivalence between ULift α and α.

                          Equations
                          • MeasurableEquiv.ulift = { toEquiv := Equiv.ulift, measurable_toFun := (_ : Measurable ULift.down), measurable_invFun := (_ : Measurable ULift.up) }
                          Instances For
                            theorem MeasurableEquiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : βγ} (e : α ≃ᵐ β) :
                            def MeasurableEquiv.ofUniqueOfUnique (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] [Unique α] [Unique β] :
                            α ≃ᵐ β

                            Any two types with unique elements are measurably equivalent.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def MeasurableEquiv.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
                              α × γ ≃ᵐ β × δ

                              Products of equivalent measurable spaces are equivalent.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def MeasurableEquiv.prodComm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
                                α × β ≃ᵐ β × α

                                Products of measurable spaces are symmetric.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def MeasurableEquiv.prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                                  (α × β) × γ ≃ᵐ α × β × γ

                                  Products of measurable spaces are associative.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def MeasurableEquiv.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
                                    α γ ≃ᵐ β δ

                                    Sums of measurable spaces are symmetric.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      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
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def MeasurableEquiv.Set.univ (α : Type u_6) [MeasurableSpace α] :
                                        Set.univ ≃ᵐ α

                                        univ α ≃ α as measurable spaces.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def MeasurableEquiv.Set.singleton {α : Type u_1} [MeasurableSpace α] (a : α) :
                                          {a} ≃ᵐ Unit

                                          {a} ≃ Unit as measurable spaces.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            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
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              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
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def MeasurableEquiv.sumProdDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                                                (α β) × γ ≃ᵐ α × γ β × γ

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

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def MeasurableEquiv.prodSumDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
                                                  α × (β γ) ≃ᵐ α × β α × γ

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

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def MeasurableEquiv.sumProdSum (α : Type u_6) (β : Type u_7) (γ : Type u_8) (δ : Type u_9) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] :
                                                    (α β) × (γ δ) ≃ᵐ (α × γ α × δ) β × γ β × δ

                                                    Products distribute over sums as measurable spaces.

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

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

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        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
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem MeasurableEquiv.coe_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] (f : δ δ') :
                                                          @[simp]
                                                          theorem MeasurableEquiv.piMeasurableEquivTProd_symm_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : List.Nodup l) (h : ∀ (i : δ'), i l) :
                                                          @[simp]
                                                          theorem MeasurableEquiv.piMeasurableEquivTProd_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : List.Nodup l) (h : ∀ (i : δ'), i l) :
                                                          def MeasurableEquiv.piMeasurableEquivTProd {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : List.Nodup l) (h : ∀ (i : δ'), i l) :
                                                          ((i : δ') → π i) ≃ᵐ List.TProd π l

                                                          Pi-types are measurably equivalent to iterated products.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem MeasurableEquiv.piUnique_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                            (MeasurableEquiv.piUnique π) = fun (f : (i : δ') → π i) => f default
                                                            @[simp]
                                                            theorem MeasurableEquiv.piUnique_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
                                                            (MeasurableEquiv.piUnique π).symm = uniqueElim
                                                            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
                                                            Instances For
                                                              @[simp]
                                                              theorem MeasurableEquiv.funUnique_symm_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                              (MeasurableEquiv.funUnique α β).symm = uniqueElim
                                                              @[simp]
                                                              theorem MeasurableEquiv.funUnique_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :
                                                              (MeasurableEquiv.funUnique α β) = fun (f : αβ) => f default
                                                              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
                                                              Instances For
                                                                @[simp]
                                                                theorem MeasurableEquiv.piFinTwo_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                (MeasurableEquiv.piFinTwo α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)
                                                                @[simp]
                                                                theorem MeasurableEquiv.piFinTwo_symm_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
                                                                (MeasurableEquiv.piFinTwo α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                                                                def MeasurableEquiv.piFinTwo (α : Fin 2Type 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
                                                                Instances For
                                                                  @[simp]
                                                                  theorem MeasurableEquiv.finTwoArrow_symm_apply {α : Type u_1} [MeasurableSpace α] :
                                                                  MeasurableEquiv.finTwoArrow.symm = fun (p : α × α) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
                                                                  @[simp]
                                                                  theorem MeasurableEquiv.finTwoArrow_apply {α : Type u_1} [MeasurableSpace α] :
                                                                  MeasurableEquiv.finTwoArrow = fun (f : Fin 2α) => (f 0, f 1)
                                                                  def MeasurableEquiv.finTwoArrow {α : Type u_1} [MeasurableSpace α] :
                                                                  (Fin 2α) ≃ᵐ α × α

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

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem MeasurableEquiv.piFinSuccAbove_apply {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
                                                                    (MeasurableEquiv.piFinSuccAbove α i) = fun (f : (j : Fin (n + 1)) → α j) => (f i, fun (j : Fin n) => f (Fin.succAbove i j))
                                                                    @[simp]
                                                                    theorem MeasurableEquiv.piFinSuccAbove_symm_apply {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
                                                                    (MeasurableEquiv.piFinSuccAbove α i).symm = fun (f : α i × ((j : Fin n) → α (Fin.succAbove i j))) => Fin.insertNth i f.1 f.2
                                                                    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) → α (Fin.succAbove i j))

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

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem MeasurableEquiv.piEquivPiSubtypeProd_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                      (MeasurableEquiv.piEquivPiSubtypeProd π p) = fun (f : (i : δ') → π i) => (fun (x : { x : δ' // p x }) => f x, fun (x : { x : δ' // ¬p x }) => f x)
                                                                      @[simp]
                                                                      theorem MeasurableEquiv.piEquivPiSubtypeProd_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [DecidablePred p] :
                                                                      (MeasurableEquiv.piEquivPiSubtypeProd π p).symm = fun (f : ((i : { x : δ' // p x }) → π i) × ((i : { x : δ' // ¬p x }) → π i)) (x : δ') => if h : p x then f.fst { val := x, property := h } else f.snd { val := x, property := h }
                                                                      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
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        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
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          theorem MeasurableEquiv.coe_sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
                                                                          theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
                                                                          def MeasurableEquiv.piFinsetUnion {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {s : Finset δ'} {t : Finset δ'} (h : Disjoint s t) :
                                                                          ((i : { x : δ' // x s }) → π i) × ((i : { x : δ' // x t }) → π i) ≃ᵐ ((i : { x : δ' // x 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
                                                                            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
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              @[simp]
                                                                              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
                                                                                @[simp]
                                                                                theorem MeasurableEquiv.ofInvolutive_apply {α : Type u_1} [MeasurableSpace α] (f : αα) (hf : Function.Involutive f) (hf' : Measurable f) (a : α) :
                                                                                @[simp]
                                                                                theorem MeasurableEquiv.ofInvolutive_symm {α : Type u_1} [MeasurableSpace α] (f : αα) (hf : Function.Involutive f) (hf' : Measurable f) :
                                                                                @[simp]
                                                                                theorem MeasurableEmbedding.comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} (hf : MeasurableEmbedding f) :
                                                                                MeasurableSpace.comap f inst✝ = inst✝¹
                                                                                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
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  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
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    theorem MeasurableEmbedding.of_measurable_inverse_on_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {g : (Set.range f)α} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g (Set.rangeFactorization f)) :
                                                                                    theorem MeasurableEmbedding.of_measurable_inverse {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {g : βα} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g f) :
                                                                                    noncomputable def MeasurableEmbedding.schroederBernstein {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : αβ} {g : βα} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g) :
                                                                                    α ≃ᵐ β

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

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      theorem MeasurableSpace.comap_compl {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [BooleanAlgebra β] (h : Measurable compl) (f : αβ) :
                                                                                      MeasurableSpace.comap (fun (a : α) => (f a)) inferInstance = MeasurableSpace.comap f inferInstance
                                                                                      @[simp]
                                                                                      theorem MeasurableSpace.comap_not {α : Type u_1} (p : αProp) :
                                                                                      MeasurableSpace.comap (fun (a : α) => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance

                                                                                      We say a measurable space is countably generated if it can be generated by a countable set of sets.

                                                                                      Instances

                                                                                        If a measurable space is countably generated and separates points, it admits a measurable injection into the Cantor space ℕ → Bool (equipped with the product sigma algebra).

                                                                                        A filter f is measurably generates if each s ∈ f includes a measurable t ∈ f.

                                                                                        Instances
                                                                                          theorem Filter.Eventually.exists_measurable_mem {α : Type u_1} [MeasurableSpace α] {f : Filter α} [Filter.IsMeasurablyGenerated f] {p : αProp} (h : ∀ᶠ (x : α) in f, p x) :
                                                                                          ∃ s ∈ f, MeasurableSet s xs, p x
                                                                                          theorem Filter.Eventually.exists_measurable_mem_of_smallSets {α : Type u_1} [MeasurableSpace α] {f : Filter α} [Filter.IsMeasurablyGenerated f] {p : Set αProp} (h : ∀ᶠ (s : Set α) in Filter.smallSets f, p s) :
                                                                                          ∃ s ∈ f, MeasurableSet s p s
                                                                                          instance Filter.iInf_isMeasurablyGenerated {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] {f : ιFilter α} [∀ (i : ι), Filter.IsMeasurablyGenerated (f i)] :
                                                                                          Filter.IsMeasurablyGenerated (⨅ (i : ι), f i)
                                                                                          Equations
                                                                                          theorem measurableSet_tendsto {β : Type u_2} {γ : Type u_3} {δ : Type u_4} :
                                                                                          ∀ {x : MeasurableSpace β} [inst : MeasurableSpace γ] [inst_1 : Countable δ] {l : Filter δ} [inst_2 : Filter.IsCountablyGenerated l] (l' : Filter γ) [inst_3 : Filter.IsCountablyGenerated l'] [hl' : Filter.IsMeasurablyGenerated l'] {f : δβγ}, (∀ (i : δ), Measurable (f i))MeasurableSet {x : β | Filter.Tendsto (fun (n : δ) => f n x) l l'}

                                                                                          The set of points for which a sequence of measurable functions converges to a given value is measurable.

                                                                                          def IsCountablySpanning {α : Type u_1} (C : Set (Set α)) :

                                                                                          We say that a collection of sets is countably spanning if a countable subset spans the whole type. This is a useful condition in various parts of measure theory. For example, it is a needed condition to show that the product of two collections generate the product sigma algebra, see generateFrom_prod_eq.

                                                                                          Equations
                                                                                          Instances For

                                                                                            Typeclasses on Subtype MeasurableSet #

                                                                                            instance MeasurableSet.Subtype.instMembership {α : Type u_1} [MeasurableSpace α] :
                                                                                            Membership α (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instMembership = { mem := fun (a : α) (s : Subtype MeasurableSet) => a s }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.mem_coe {α : Type u_1} [MeasurableSpace α] (a : α) (s : Subtype MeasurableSet) :
                                                                                            a s a s
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instEmptyCollection = { emptyCollection := { val := , property := (_ : MeasurableSet ) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_empty {α : Type u_1} [MeasurableSpace α] :
                                                                                            =
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instInsert = { insert := fun (a : α) (s : Subtype MeasurableSet) => { val := insert a s, property := (_ : MeasurableSet (insert a s)) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Subtype MeasurableSet) :
                                                                                            (insert a s) = insert a s
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instSingleton = { singleton := fun (a : α) => { val := {a}, property := (_ : MeasurableSet {a}) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :
                                                                                            {a} = {a}
                                                                                            Equations
                                                                                            instance MeasurableSet.Subtype.instHasCompl {α : Type u_1} [MeasurableSpace α] :
                                                                                            HasCompl (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instHasCompl = { compl := fun (x : Subtype MeasurableSet) => { val := (x), property := (_ : MeasurableSet (x)) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_compl {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) :
                                                                                            s = (s)
                                                                                            instance MeasurableSet.Subtype.instUnion {α : Type u_1} [MeasurableSpace α] :
                                                                                            Union (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instUnion = { union := fun (x y : Subtype MeasurableSet) => { val := x y, property := (_ : MeasurableSet (x y)) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_union {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
                                                                                            (s t) = s t
                                                                                            instance MeasurableSet.Subtype.instSup {α : Type u_1} [MeasurableSpace α] :
                                                                                            Sup (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instSup = { sup := fun (x y : Subtype MeasurableSet) => x y }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.sup_eq_union {α : Type u_1} [MeasurableSpace α] (s : { s : Set α // MeasurableSet s }) (t : { s : Set α // MeasurableSet s }) :
                                                                                            s t = s t
                                                                                            instance MeasurableSet.Subtype.instInter {α : Type u_1} [MeasurableSpace α] :
                                                                                            Inter (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instInter = { inter := fun (x y : Subtype MeasurableSet) => { val := x y, property := (_ : MeasurableSet (x y)) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_inter {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
                                                                                            (s t) = s t
                                                                                            instance MeasurableSet.Subtype.instInf {α : Type u_1} [MeasurableSpace α] :
                                                                                            Inf (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instInf = { inf := fun (x y : Subtype MeasurableSet) => x y }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.inf_eq_inter {α : Type u_1} [MeasurableSpace α] (s : { s : Set α // MeasurableSet s }) (t : { s : Set α // MeasurableSet s }) :
                                                                                            s t = s t
                                                                                            instance MeasurableSet.Subtype.instSDiff {α : Type u_1} [MeasurableSpace α] :
                                                                                            SDiff (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instSDiff = { sdiff := fun (x y : Subtype MeasurableSet) => { val := x \ y, property := (_ : MeasurableSet (x \ y)) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_sdiff {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
                                                                                            (s \ t) = s \ t
                                                                                            instance MeasurableSet.Subtype.instBot {α : Type u_1} [MeasurableSpace α] :
                                                                                            Bot (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instBot = { bot := }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_bot {α : Type u_1} [MeasurableSpace α] :
                                                                                            =
                                                                                            instance MeasurableSet.Subtype.instTop {α : Type u_1} [MeasurableSpace α] :
                                                                                            Top (Subtype MeasurableSet)
                                                                                            Equations
                                                                                            • MeasurableSet.Subtype.instTop = { top := { val := Set.univ, property := (_ : MeasurableSet Set.univ) } }
                                                                                            @[simp]
                                                                                            theorem MeasurableSet.coe_top {α : Type u_1} [MeasurableSpace α] :
                                                                                            =
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            theorem MeasurableSet.measurableSet_blimsup {α : Type u_1} [MeasurableSpace α] {s : Set α} {p : Prop} (h : ∀ (n : ), p nMeasurableSet (s n)) :
                                                                                            MeasurableSet (Filter.blimsup s Filter.atTop p)
                                                                                            theorem MeasurableSet.measurableSet_bliminf {α : Type u_1} [MeasurableSpace α] {s : Set α} {p : Prop} (h : ∀ (n : ), p nMeasurableSet (s n)) :
                                                                                            MeasurableSet (Filter.bliminf s Filter.atTop p)
                                                                                            theorem MeasurableSet.measurableSet_limsup {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : ∀ (n : ), MeasurableSet (s n)) :
                                                                                            MeasurableSet (Filter.limsup s Filter.atTop)
                                                                                            theorem MeasurableSet.measurableSet_liminf {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : ∀ (n : ), MeasurableSet (s n)) :
                                                                                            MeasurableSet (Filter.liminf s Filter.atTop)