Measurable finite partitions

This file records elementary ways to construct measurable finite partitions and shows that measurability passes from a finer finite partition to a coarser one. It also makes the canonical map from a point to its finite-partition index measurable and packages the canonical finite partitions of a countably generated measurable space as Finpartitions.

theorem Finpartition.measurable_indexedPartition_index {Ω : Type u_1} [MeasurableSpace Ω] (P : Finpartition Set.univ) [MeasurableSpace ↥P.parts] (hP : ∀ p ∈ P.parts, MeasurableSet p) : Measurable P.indexedPartition.index

The map sending a point to its part in a measurable finite partition is measurable, for any measurable space structure on the finite type of parts — in particular for the discrete one. Countability of the parts is what makes an arbitrary structure on them admissible: measurability of the fibres already forces measurability of every preimage.

theorem Finpartition.comap_indexedPartition_index_top {Ω : Type u_1} (P : Finpartition Set.univ) : MeasurableSpace.comap P.indexedPartition.index ⊤ = MeasurableSpace.generateFrom ↑P.parts

The σ-algebra generated by the parts of a finite partition is the pullback of the discrete σ-algebra along the map sending a point to its part.

noncomputable def Finpartition.countablePartition (Ω : Type u_2) [MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] (n : ℕ) : Finpartition Set.univ

The canonical finite partition at level n of a countably generated measurable space.

Its nonempty parts are Mathlib's MeasurableSpace.countablePartition Ω n; the empty member of that set-valued partition is discarded, as required by Finpartition.

Equations

• Finpartition.countablePartition Ω n = (Finpartition.ofPairwiseDisjoint ⋯.toFinset ⋯).copy ⋯

@[simp]

theorem Finpartition.parts_countablePartition (Ω : Type u_2) [MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] (n : ℕ) : (countablePartition Ω n).parts = ⋯.toFinset.erase ∅

The parts of the canonical Finpartition are the nonempty members of Mathlib's canonical finite set-valued partition.

theorem Finpartition.countablePartition_antitone (Ω : Type u_2) [MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] : Antitone (countablePartition Ω)

The canonical finite partitions become finer as the level increases.

theorem Finpartition.measurableSet_of_mem_countablePartition (Ω : Type u_2) [MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] (n : ℕ) {s : Set Ω} (hs : s ∈ (countablePartition Ω n).parts) : MeasurableSet s

Every part of the canonical finite partition of a countably generated measurable space is measurable.

theorem Finpartition.comap_countablePartition_index_top (Ω : Type u_2) [MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] (n : ℕ) : MeasurableSpace.comap (countablePartition Ω n).indexedPartition.index ⊤ = MeasurableSpace.generateFrom (MeasurableSpace.countablePartition Ω n)

The index map of the canonical finite partition generates Mathlib's canonical finite σ-algebra at the same level.

theorem Finpartition.measurableSet_of_mem_bipartition {Ω : Type u_1} [MeasurableSpace Ω] {s p : Set Ω} (hs : MeasurableSet s) (hp : p ∈ (bipartition s).parts) : MeasurableSet p

Every part of a bipartition along a measurable set is measurable.

theorem Finpartition.measurableSet_of_mem_inf {Ω : Type u_1} [MeasurableSpace Ω] {u : Set Ω} {P Q : Finpartition u} (hP : ∀ p ∈ P.parts, MeasurableSet p) (hQ : ∀ q ∈ Q.parts, MeasurableSet q) {r : Set Ω} (hr : r ∈ (P ⊓ Q).parts) : MeasurableSet r

The common refinement of two measurable finite partitions is measurable.

theorem Finpartition.measurableSet_of_mem_of_le {Ω : Type u_1} [MeasurableSpace Ω] {u : Set Ω} {P Q : Finpartition u} (hQ : ∀ q ∈ Q.parts, MeasurableSet q) (href : Q ≤ P) {p : Set Ω} (hp : p ∈ P.parts) : MeasurableSet p

A part of a finite partition is measurable when it is a union of parts of a measurable refinement.