Documentation

Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Countably generated measurable spaces #

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

In such a space, we can also build a sequence of finer and finer finite measurable partitions of the space such that the measurable space is generated by the union of all partitions.

Main definitions #

Main statements #

The file also contains measurability results about memPartition, from which the properties of countablePartition are deduced.

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

Instances

    A countable set of sets that generate the measurable space. We insert to ensure it is nonempty.

    Equations
    Instances For

      A countable sequence of sets generating the measurable space.

      Equations
      Instances For

        We say that a measurable space separates points if for any two distinct points, there is a measurable set containing one but not the other.

        Instances
          theorem MeasurableSpace.separatesPoints_def {α : Type u_1} [MeasurableSpace α] [hs : MeasurableSpace.SeparatesPoints α] {x : α} {y : α} (h : ∀ (s : Set α), MeasurableSet sx sy s) :
          x = y
          theorem MeasurableSpace.exists_measurableSet_of_ne {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x : α} {y : α} (h : x y) :
          ∃ (s : Set α), MeasurableSet s x s ys
          theorem MeasurableSpace.separating_of_generateFrom {α : Type u_1} (S : Set (Set α)) [h : MeasurableSpace.SeparatesPoints α] (x : α) (y : α) :
          (sS, x s y s)x = y

          If the measurable space generated by S separates points, then this is witnessed by sets in S.

          If a measurable space admits a countable separating family of measurable sets, there is a countably generated coarser space which still separates points.

          noncomputable def MeasurableSpace.mapNatBool (α : Type u_1) [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (x : α) (n : ) :

          A map from a measurable space to the Cantor space ℕ → Bool induced by a countable sequence of sets generating the measurable space.

          Equations
          Instances For

            If a measurable space is countably generated and separates points, it is measure equivalent to some some subset of the Cantor space ℕ → Bool (equipped with the product sigma algebra). Note: s need not be measurable, so this map need not be a MeasurableEmbedding to the Cantor Space.

            If a measurable space admits a countable sequence of measurable sets separating points, it admits a measurable injection into the Cantor space ℕ → Bool (equipped with the product sigma algebra).

            theorem MeasurableSpace.measurableSet_succ_memPartition {α : Type u_1} (t : Set α) (n : ) {s : Set α} (hs : s memPartition t n) :
            theorem MeasurableSpace.measurableSet_generateFrom_memPartition_iff {α : Type u_1} (t : Set α) (n : ) (s : Set α) :
            MeasurableSet s ∃ (S : Finset (Set α)), S memPartition t n s = ⋃₀ S
            theorem MeasurableSpace.measurableSet_memPartition {α : Type u_1} [MeasurableSpace α] {t : Set α} (ht : ∀ (n : ), MeasurableSet (t n)) (n : ) {s : Set α} (hs : s memPartition t n) :
            theorem MeasurableSpace.measurableSet_memPartitionSet {α : Type u_1} [MeasurableSpace α] {t : Set α} (ht : ∀ (n : ), MeasurableSet (t n)) (n : ) (a : α) :

            For each n : ℕ, countablePartition α n is a partition of the space in at most 2^n sets. Each partition is finer than the preceeding one. The measurable space generated by the union of all those partitions is the measurable space on α.

            Equations
            Instances For

              The set in countablePartition α n to which a : α belongs.

              Equations
              Instances For