Square filtrations from finite measurable partitions

The canonical finite partitions of a countably generated measurable space give a filtration on its square by recording the partition part of each coordinate. These square σ-algebras increase to the full product σ-algebra. This is the filtration naturally used by block-average approximations of measurable kernels.

Main results

• TauCeti.MeasureTheory.countableSquareFiltration is the filtration by equal-level product partitions.
• TauCeti.MeasureTheory.iSup_countableSquareFiltration says that it generates the product σ-algebra.
• TauCeti.MeasureTheory.countableSquareFiltration_eq_comap identifies each level with the information carried by the pair of finite-partition indices.

noncomputable def TauCeti.MeasureTheory.countableSquareFiltration (Ω : Type u_2) [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] : MeasureTheory.Filtration ℕ (m.prod m)

The filtration on Ω × Ω whose level n is the product of the level-n canonical finite σ-algebra on each coordinate.

Equations

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

@[simp]

theorem TauCeti.MeasureTheory.countableSquareFiltration_apply {Ω : Type u_1} [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] (n : ℕ) : ↑(countableSquareFiltration Ω) n = (↑(ProbabilityTheory.countableFiltration Ω) n).prod (↑(ProbabilityTheory.countableFiltration Ω) n)

A level of the square filtration is the product of the corresponding canonical finite σ-algebra with itself.

theorem TauCeti.MeasureTheory.iSup_countableSquareFiltration {Ω : Type u_1} [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] : ⨆ (n : ℕ), ↑(countableSquareFiltration Ω) n = m.prod m

The equal-level square filtration generates the full product σ-algebra.

theorem TauCeti.MeasureTheory.countableSquareFiltration_eq_comap {Ω : Type u_1} [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] (n : ℕ) : ↑(countableSquareFiltration Ω) n = MeasurableSpace.comap (Prod.map (Finpartition.countablePartition Ω n).indexedPartition.index (Finpartition.countablePartition Ω n).indexedPartition.index) ⊤

A level of the square filtration is precisely the information carried by the two canonical finite-partition indices.