Documentation

Mathlib.MeasureTheory.MeasurableSpace.Defs

Measurable spaces and measurable functions #

This file defines measurable spaces and measurable functions.

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.

References #

Tags #

measurable space, σ-algebra, measurable function

class MeasurableSpace (α : Type u_7) :
Type u_7

A measurable space is a space equipped with a σ-algebra.

  • MeasurableSet' : Set αProp

    Predicate saying that a given set is measurable. Use MeasurableSet in the root namespace instead.

  • measurableSet_empty : self.MeasurableSet'

    The empty set is a measurable set. Use MeasurableSet.empty instead.

  • measurableSet_compl : ∀ (s : Set α), self.MeasurableSet' sself.MeasurableSet' s

    The complement of a measurable set is a measurable set. Use MeasurableSet.compl instead.

  • measurableSet_iUnion : ∀ (f : Set α), (∀ (i : ), self.MeasurableSet' (f i))self.MeasurableSet' (⋃ (i : ), f i)

    The union of a sequence of measurable sets is a measurable set. Use a more general MeasurableSet.iUnion instead.

Instances
    theorem MeasurableSpace.measurableSet_empty {α : Type u_7} (self : MeasurableSpace α) :
    self.MeasurableSet'

    The empty set is a measurable set. Use MeasurableSet.empty instead.

    theorem MeasurableSpace.measurableSet_compl {α : Type u_7} (self : MeasurableSpace α) (s : Set α) :
    self.MeasurableSet' sself.MeasurableSet' s

    The complement of a measurable set is a measurable set. Use MeasurableSet.compl instead.

    theorem MeasurableSpace.measurableSet_iUnion {α : Type u_7} (self : MeasurableSpace α) (f : Set α) :
    (∀ (i : ), self.MeasurableSet' (f i))self.MeasurableSet' (⋃ (i : ), f i)

    The union of a sequence of measurable sets is a measurable set. Use a more general MeasurableSet.iUnion instead.

    Equations
    • instMeasurableSpaceOrderDual = h
    def MeasurableSet {α : Type u_1} [MeasurableSpace α] (s : Set α) :

    MeasurableSet s means that s is measurable (in the ambient measure space on α)

    Equations
    Instances For

      Notation for MeasurableSet with respect to a non-standard σ-algebra.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem MeasurableSet.compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} :
        theorem MeasurableSet.of_compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} (h : MeasurableSet s) :
        @[simp]
        @[simp]
        theorem MeasurableSet.univ {α : Type u_1} {m : MeasurableSpace α} :
        MeasurableSet Set.univ
        theorem MeasurableSet.congr {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (h : s = t) :
        theorem MeasurableSet.iUnion {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] ⦃f : ιSet α (h : ∀ (b : ι), MeasurableSet (f b)) :
        MeasurableSet (⋃ (b : ι), f b)
        theorem MeasurableSet.biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : βSet α} {s : Set β} (hs : s.Countable) (h : bs, MeasurableSet (f b)) :
        MeasurableSet (bs, f b)
        theorem Set.Finite.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : βSet α} {s : Set β} (hs : s.Finite) (h : bs, MeasurableSet (f b)) :
        MeasurableSet (bs, f b)
        theorem Finset.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : βSet α} (s : Finset β) (h : bs, MeasurableSet (f b)) :
        MeasurableSet (bs, f b)
        theorem MeasurableSet.sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Countable) (h : ts, MeasurableSet t) :
        theorem Set.Finite.measurableSet_sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Finite) (h : ts, MeasurableSet t) :
        theorem MeasurableSet.iInter {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] {f : ιSet α} (h : ∀ (b : ι), MeasurableSet (f b)) :
        MeasurableSet (⋂ (b : ι), f b)
        theorem MeasurableSet.biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : βSet α} {s : Set β} (hs : s.Countable) (h : bs, MeasurableSet (f b)) :
        MeasurableSet (bs, f b)
        theorem Set.Finite.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : βSet α} {s : Set β} (hs : s.Finite) (h : bs, MeasurableSet (f b)) :
        MeasurableSet (bs, f b)
        theorem Finset.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : βSet α} (s : Finset β) (h : bs, MeasurableSet (f b)) :
        MeasurableSet (bs, f b)
        theorem MeasurableSet.sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Countable) (h : ts, MeasurableSet t) :
        theorem Set.Finite.measurableSet_sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Finite) (h : ts, MeasurableSet t) :
        @[simp]
        theorem MeasurableSet.union {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
        MeasurableSet (s₁ s₂)
        @[simp]
        theorem MeasurableSet.inter {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
        MeasurableSet (s₁ s₂)
        @[simp]
        theorem MeasurableSet.diff {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
        MeasurableSet (s₁ \ s₂)
        @[simp]
        theorem MeasurableSet.himp {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
        MeasurableSet (s₁ s₂)
        @[simp]
        theorem MeasurableSet.symmDiff {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
        @[simp]
        theorem MeasurableSet.bihimp {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
        MeasurableSet (bihimp s₁ s₂)
        @[simp]
        theorem MeasurableSet.ite {α : Type u_1} {m : MeasurableSpace α} {t : Set α} {s₁ : Set α} {s₂ : Set α} (ht : MeasurableSet t) (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
        MeasurableSet (t.ite s₁ s₂)
        theorem MeasurableSet.ite' {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} {p : Prop} (hs : pMeasurableSet s) (ht : ¬pMeasurableSet t) :
        MeasurableSet (if p then s else t)
        @[simp]
        theorem MeasurableSet.cond {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) {i : Bool} :
        MeasurableSet (bif i then s₁ else s₂)
        @[simp]
        theorem MeasurableSet.disjointed {α : Type u_1} {m : MeasurableSpace α} {f : Set α} (h : ∀ (i : ), MeasurableSet (f i)) (n : ) :
        theorem MeasurableSet.const {α : Type u_1} {m : MeasurableSpace α} (p : Prop) :
        MeasurableSet {_a : α | p}
        theorem nonempty_measurable_superset {α : Type u_1} {m : MeasurableSpace α} (s : Set α) :
        Nonempty { t : Set α // s t MeasurableSet t }

        Every set has a measurable superset. Declare this as local instance as needed.

        theorem MeasurableSpace.ext {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} (h : ∀ (s : Set α), MeasurableSet s MeasurableSet s) :
        m₁ = m₂
        theorem MeasurableSpace.ext_iff {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} :
        m₁ = m₂ ∀ (s : Set α), MeasurableSet s MeasurableSet s

        A typeclass mixin for MeasurableSpaces such that each singleton is measurable.

        • measurableSet_singleton : ∀ (x : α), MeasurableSet {x}

          A singleton is a measurable set.

        Instances

          A singleton is a measurable set.

          theorem measurableSet_eq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} :
          MeasurableSet {x : α | x = a}
          theorem MeasurableSet.insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : MeasurableSet s) (a : α) :
          @[simp]
          theorem Set.Subsingleton.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Subsingleton) :
          theorem Set.Finite.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Finite) :
          theorem Set.Countable.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Countable) :
          def MeasurableSpace.copy {α : Type u_1} (m : MeasurableSpace α) (p : Set αProp) (h : ∀ (s : Set α), p s MeasurableSet s) :

          Copy of a MeasurableSpace with a new MeasurableSet equal to the old one. Useful to fix definitional equalities.

          Equations
          • m.copy p h = { MeasurableSet' := p, measurableSet_empty := , measurableSet_compl := , measurableSet_iUnion := }
          Instances For
            theorem MeasurableSpace.measurableSet_copy {α : Type u_1} {m : MeasurableSpace α} {p : Set αProp} (h : ∀ (s : Set α), p s MeasurableSet s) {s : Set α} :
            theorem MeasurableSpace.copy_eq {α : Type u_1} {m : MeasurableSpace α} {p : Set αProp} (h : ∀ (s : Set α), p s MeasurableSet s) :
            m.copy p h = m
            instance MeasurableSpace.instLE {α : Type u_1} :
            Equations
            theorem MeasurableSpace.le_def {α : Type u_7} {a : MeasurableSpace α} {b : MeasurableSpace α} :
            a b a.MeasurableSet' b.MeasurableSet'
            Equations
            inductive MeasurableSpace.GenerateMeasurable {α : Type u_1} (s : Set (Set α)) :
            Set αProp

            The smallest σ-algebra containing a collection s of basic sets

            Instances For

              Construct the smallest measure space containing a collection of basic sets

              Equations
              Instances For
                theorem MeasurableSpace.measurableSet_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t s) :
                theorem MeasurableSpace.generateFrom_induction {α : Type u_1} (p : Set αProp) (C : Set (Set α)) (hC : tC, p t) (h_empty : p ) (h_compl : ∀ (t : Set α), p tp t) (h_Union : ∀ (f : Set α), (∀ (n : ), p (f n))p (⋃ (i : ), f i)) {s : Set α} (hs : MeasurableSet s) :
                p s
                theorem MeasurableSpace.generateFrom_le {α : Type u_1} {s : Set (Set α)} {m : MeasurableSpace α} (h : ts, MeasurableSet t) :
                theorem MeasurableSpace.forall_generateFrom_mem_iff_mem_iff {α : Type u_1} {S : Set (Set α)} {x : α} {y : α} :
                (∀ (s : Set α), MeasurableSet s(x s y s)) sS, x s y s
                def MeasurableSpace.mkOfClosure {α : Type u_1} (g : Set (Set α)) (hg : {t : Set α | MeasurableSet t} = g) :

                If g is a collection of subsets of α such that the σ-algebra generated from g contains the same sets as g, then g was already a σ-algebra.

                Equations
                Instances For
                  def MeasurableSpace.giGenerateFrom {α : Type u_1} :
                  GaloisInsertion MeasurableSpace.generateFrom fun (m : MeasurableSpace α) => {t : Set α | MeasurableSet t}

                  We get a Galois insertion between σ-algebras on α and Set (Set α) by using generate_from on one side and the collection of measurable sets on the other side.

                  Equations
                  Instances For
                    Equations
                    • MeasurableSpace.instCompleteLattice = MeasurableSpace.giGenerateFrom.liftCompleteLattice
                    Equations
                    • MeasurableSpace.instInhabited = { default := }
                    theorem MeasurableSpace.iSup_generateFrom {α : Type u_1} {ι : Sort u_6} (s : ιSet (Set α)) :
                    ⨆ (i : ι), MeasurableSpace.generateFrom (s i) = MeasurableSpace.generateFrom (⋃ (i : ι), s i)
                    theorem MeasurableSpace.measurableSet_bot_iff {α : Type u_1} {s : Set α} :
                    MeasurableSet s s = s = Set.univ
                    @[simp]
                    @[simp]
                    theorem MeasurableSpace.measurableSet_sInf {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α} :
                    MeasurableSet s mms, MeasurableSet s
                    theorem MeasurableSpace.measurableSet_iInf {α : Type u_1} {ι : Sort u_7} {m : ιMeasurableSpace α} {s : Set α} :
                    MeasurableSet s ∀ (i : ι), MeasurableSet s
                    theorem MeasurableSpace.measurableSet_sup {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {s : Set α} :
                    MeasurableSet s MeasurableSpace.GenerateMeasurable (MeasurableSet MeasurableSet) s
                    theorem MeasurableSpace.measurableSet_iSup {α : Type u_1} {ι : Sort u_7} {m : ιMeasurableSpace α} {s : Set α} :
                    theorem MeasurableSpace.measurableSpace_iSup_eq {α : Type u_1} {ι : Sort u_6} (m : ιMeasurableSpace α) :
                    ⨆ (n : ι), m n = MeasurableSpace.generateFrom {s : Set α | ∃ (n : ι), MeasurableSet s}
                    theorem MeasurableSpace.generateFrom_iUnion_measurableSet {α : Type u_1} {ι : Sort u_6} (m : ιMeasurableSpace α) :
                    MeasurableSpace.generateFrom (⋃ (n : ι), {t : Set α | MeasurableSet t}) = ⨆ (n : ι), m n
                    def Measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : αβ) :

                    A function f between measurable spaces is measurable if the preimage of every measurable set is measurable.

                    Equations
                    Instances For

                      Notation for Measurable with respect to a non-standanrd σ-algebra in the domain.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem measurable_id {α : Type u_1} :
                        ∀ {x : MeasurableSpace α}, Measurable id
                        theorem measurable_id' {α : Type u_1} :
                        ∀ {x : MeasurableSpace α}, Measurable fun (a : α) => a
                        theorem Measurable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
                        ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : βγ} {f : αβ}, Measurable gMeasurable fMeasurable (g f)
                        theorem Measurable.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
                        ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : βγ} {f : αβ}, Measurable gMeasurable fMeasurable fun (x : α) => g (f x)
                        @[simp]
                        theorem measurable_const {α : Type u_1} {β : Type u_2} :
                        ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {a : α}, Measurable fun (x : β) => a
                        theorem Measurable.le {β : Type u_2} {α : Type u_7} {m : MeasurableSpace α} {m0 : MeasurableSpace α} :
                        ∀ {x : MeasurableSpace β}, m m0∀ {f : αβ}, Measurable fMeasurable f

                        A typeclass mixin for MeasurableSpaces such that all sets are measurable.

                        Instances
                          Equations
                          • =
                          theorem measurable_discrete {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace α] (f : αβ) :
                          @[instance 100]

                          Warning: Creates a typeclass loop with MeasurableSingletonClass.toDiscreteMeasurableSpace. To be monitored.

                          Equations
                          • =