# 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 `α`.

source
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' := ⋯ }

Instances For

source
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
source
theorem ProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) (a : α) :
MeasurableSet (memPartitionSet t n a)
source
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, ⋯⟩
source
theorem ProbabilityTheory.measurable_partitionFiltration_memPartitionSet {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) :
Measurable (memPartitionSet t n)
source
theorem ProbabilityTheory.measurable_memPartitionSet {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) :
Measurable (memPartitionSet t n)
source
theorem ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) :
⨆ (n : ℕ), ↑(partitionFiltration ht) n = MeasurableSpace.generateFrom (Set.range t)
source
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 : ℕ), ↑(partitionFiltration ht) n = m
source
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' := ⋯ }

Instances For

source
theorem ProbabilityTheory.measurableSet_countableFiltration_of_mem {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) {s : Set α} (hs : s ∈ MeasurableSpace.countablePartition α n) :
MeasurableSet s
source
theorem ProbabilityTheory.measurableSet_countableFiltration_countablePartitionSet {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) (t : α) :
MeasurableSet (MeasurableSpace.countablePartitionSet n t)
source
theorem ProbabilityTheory.measurable_countablePartitionSet_subtype {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) (m : MeasurableSpace ↑(MeasurableSpace.countablePartition α n)) :
Measurable fun (a : α) => ⟨MeasurableSpace.countablePartitionSet n a, ⋯⟩
source
theorem ProbabilityTheory.measurable_countableFiltration_countablePartitionSet (α : Type u_2) [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) :
Measurable (MeasurableSpace.countablePartitionSet n)
source
theorem ProbabilityTheory.measurable_countablePartitionSet (α : Type u_2) [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) :
Measurable (MeasurableSpace.countablePartitionSet n)
source
theorem ProbabilityTheory.iSup_countableFiltration (α : Type u_2) [m : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] :
⨆ (n : ℕ), ↑(countableFiltration α) n = m