Bases of the indexed product σ-algebra

In this file we prove several versions of the following lemma:

given a finite indexed collection of measurable spaces α i, if the σ-algebra on each α i is generated by C i, then the sets {x | ∀ i, x i ∈ s i}, where s i ∈ C i, generate the σ-algebra on the indexed product of α is.

We start with some measurability properties

theorem MeasurableSpace.pi_eq_generateFrom_projections {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)} : pi = generateFrom {B : Set ((x : ι) → α x) | ∃ (i : ι) (A : Set (α i)), MeasurableSet A ∧ Function.eval i ⁻¹' A = B}

theorem IsPiSystem.pi {ι : Type u_1} {α : ι → Type u_2} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsPiSystem (C i)) : IsPiSystem (Set.univ.pi '' Set.univ.pi C)

Boxes formed by π-systems form a π-system.

theorem isPiSystem_pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] : IsPiSystem (Set.univ.pi '' Set.univ.pi fun (i : ι) => {s : Set (α i) | MeasurableSet s})

Boxes form a π-system.

theorem IsCountablySpanning.pi {ι : Type u_1} {α : ι → Type u_2} [Finite ι] {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsCountablySpanning (C i)) : IsCountablySpanning (Set.univ.pi '' Set.univ.pi C)

Boxes of countably spanning sets are countably spanning.

theorem generateFrom_pi_eq {ι : Type u_1} {α : ι → Type u_2} [Finite ι] {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsCountablySpanning (C i)) : MeasurableSpace.pi = MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C)

The product of generated σ-algebras is the one generated by boxes, if both generating sets are countably spanning.

theorem generateFrom_eq_pi {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [h : (i : ι) → MeasurableSpace (α i)] {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), MeasurableSpace.generateFrom (C i) = h i) (h2C : ∀ (i : ι), IsCountablySpanning (C i)) : MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C) = MeasurableSpace.pi

If C and D generate the σ-algebras on α resp. β, then rectangles formed by C and D generate the σ-algebra on α × β.

theorem generateFrom_pi {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [(i : ι) → MeasurableSpace (α i)] : MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi fun (i : ι) => {s : Set (α i) | MeasurableSet s}) = MeasurableSpace.pi

The product σ-algebra is generated from boxes, i.e. s ×ˢ t for sets s : set α and t : set β.