Documentation

Mathlib.MeasureTheory.Category.MeasCat

The category of measurable spaces #

Measurable spaces and measurable functions form a (concrete) category MeasCat.

Main definitions #

Tags #

measurable space, giry monad, borel

def MeasCat :
Type (u + 1)

The category of measurable spaces and measurable functions.

Equations
Instances For
    Equations
    Equations
    • X.instMeasurableSpaceα = X.str
    def MeasCat.of (α : Type u) [ms : MeasurableSpace α] :

    Construct a bundled MeasCat from the underlying type and the typeclass.

    Equations
    Instances For
      @[simp]
      theorem MeasCat.coe_of (X : Type u) [MeasurableSpace X] :
      (MeasCat.of X) = X

      Measure X is the measurable space of measures over the measurable space X. It is the weakest measurable space, s.t. fun μ ↦ μ s is measurable for all measurable sets s in X. An important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad, the pure values are the Dirac measure, and the bind operation maps to the integral: (μ >>= ν) s = ∫ x. (ν x) s dμ.

      In probability theory, the MeasCat-morphisms X → Prob X are (sub-)Markov kernels (here Prob is the restriction of Measure to (sub-)probability space.)

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

        The Giry monad, i.e. the monadic structure associated with Measure.

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

          An example for an algebra on Measure: the nonnegative Lebesgue integral is a hom, behaving nicely under the monad operations.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible, inline]

            The Borel functor, the canonical embedding of topological spaces into measurable spaces.

            Equations
            Instances For