Filtration built from the finite partitions of a countably generated measurable space

In a countably generated measurable space α, we can 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. This sequence of partitions is defined in MeasureTheory.MeasurableSpace.CountablyGenerated.

Here, we build the filtration of the measurable spaces generated by countablePartition α n for all n : ℕ, which we call countableFiltration α. Since each measurable space in the filtration is finite, we can easily build measurable functions on those spaces. A potential application of countableFiltration α is to build a martingale with respect to that filtration and use the martingale convergence theorems to define a measurable function on α.

Main definitions

• ProbabilityTheory.partitionFiltration: for a sequence of sets t : ℕ → Set α, a filtration built from the measurable spaces generated by memPartition t n for all n : ℕ.
• ProbabilityTheory.countableFiltration: A filtration built from the measurable spaces generated by countablePartition α n for all n : ℕ.

Main statements

• ProbabilityTheory.iSup_partitionFiltration: ⨆ n, partitionFiltration α n is the measurable space on α.

def ProbabilityTheory.partitionFiltration {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) : MeasureTheory.Filtration ℕ m

A filtration built from the measurable spaces generated by the partitions memPartition t n for all n : ℕ.

Equations

• ProbabilityTheory.partitionFiltration ht = { seq := fun (n : ℕ) => MeasurableSpace.generateFrom (memPartition t n), mono' := ⋯, le' := ⋯ }

theorem ProbabilityTheory.measurableSet_partitionFiltration_of_mem {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) {s : Set α} (hs : s ∈ memPartition t n) : MeasurableSet s

theorem ProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) (a : α) : MeasurableSet (memPartitionSet t n a)

theorem ProbabilityTheory.measurable_memPartitionSet_subtype {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) (m✝ : MeasurableSpace ↑(memPartition t n)) : Measurable fun (a : α) => ⟨memPartitionSet t n a, ⋯⟩

theorem ProbabilityTheory.measurable_partitionFiltration_memPartitionSet {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) : Measurable (memPartitionSet t n)

theorem ProbabilityTheory.measurable_memPartitionSet {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) : Measurable (memPartitionSet t n)

theorem ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) : ⨆ (n : ℕ), ↑(ProbabilityTheory.partitionFiltration ht) n = MeasurableSpace.generateFrom (Set.range t)

theorem ProbabilityTheory.iSup_partitionFiltration {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (ht_range : MeasurableSpace.generateFrom (Set.range t) = m) : ⨆ (n : ℕ), ↑(ProbabilityTheory.partitionFiltration ht) n = m

def ProbabilityTheory.countableFiltration (α : Type u_2) [m : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : MeasureTheory.Filtration ℕ m

A filtration built from the measurable spaces generated by countablePartition α n for all n : ℕ.

Equations

• ProbabilityTheory.countableFiltration α = { seq := fun (n : ℕ) => MeasurableSpace.generateFrom (MeasurableSpace.countablePartition α n), mono' := ⋯, le' := ⋯ }

theorem ProbabilityTheory.measurableSet_countableFiltration_of_mem {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) {s : Set α} (hs : s ∈ MeasurableSpace.countablePartition α n) : MeasurableSet s

theorem ProbabilityTheory.measurableSet_countableFiltration_countablePartitionSet {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) (t : α) : MeasurableSet (MeasurableSpace.countablePartitionSet n t)

theorem ProbabilityTheory.measurable_countablePartitionSet_subtype {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) (m : MeasurableSpace ↑(MeasurableSpace.countablePartition α n)) : Measurable fun (a : α) => ⟨MeasurableSpace.countablePartitionSet n a, ⋯⟩

theorem ProbabilityTheory.measurable_countableFiltration_countablePartitionSet (α : Type u_2) [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) : Measurable (MeasurableSpace.countablePartitionSet n)

theorem ProbabilityTheory.measurable_countablePartitionSet (α : Type u_2) [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) : Measurable (MeasurableSpace.countablePartitionSet n)

theorem ProbabilityTheory.iSup_countableFiltration (α : Type u_2) [m : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : ⨆ (n : ℕ), ↑(ProbabilityTheory.countableFiltration α) n = m