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
        @[instance 100]

        Any measurable space structure on a countable space is countably generated.

        Equations
        • =

        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.separates {α : Type u_3} {m : MeasurableSpace α} [self : MeasurableSpace.SeparatesPoints α] (x : α) (y : α) :
          (∀ (s : Set α), MeasurableSet sx sy s)x = y
          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.separatesPoints_iff {α : Type u_1} [MeasurableSpace α] :
          MeasurableSpace.SeparatesPoints α ∀ (x y : α), (∀ (s : Set α), MeasurableSet s(x s y s))x = y
          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.

          We say that a measurable space is countably separated if there is a countable sequence of measurable sets separating points.

          Instances
            @[instance 100]
            Equations
            • =

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

                  A class registering that either α is countable or β is a countably generated measurable space.

                  Instances