The product sigma algebra

This file talks about the measurability of operations on binary functions.

theorem generateFrom_prod_eq {α : Type u_3} {β : Type u_4} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C) (hD : IsCountablySpanning D) : Prod.instMeasurableSpace = MeasurableSpace.generateFrom (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D)

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

theorem generateFrom_eq_prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {C : Set (Set α)} {D : Set (Set β)} (hC : MeasurableSpace.generateFrom C = inst✝) (hD : MeasurableSpace.generateFrom D = inst✝¹) (h2C : IsCountablySpanning C) (h2D : IsCountablySpanning D) : MeasurableSpace.generateFrom (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D) = Prod.instMeasurableSpace

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

theorem generateFrom_prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : MeasurableSpace.generateFrom (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}) = Prod.instMeasurableSpace

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

theorem isPiSystem_prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] : IsPiSystem (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})

Rectangles form a π-system.

theorem MeasurableSpace.comap_prodMk {α : Type u_3} {β : Type u_4} {γ : Type u_5} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (X : α → β) (Y : α → γ) : MeasurableSpace.comap (fun (ω : α) => (X ω, Y ω)) (mβ.prod mγ) = MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ

The comap of a product is the supremum of the comaps.

theorem MeasurableSpace.comap_prodMap {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (X : γ → α) (Y : δ → β) : MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)

The comap of Prod.map is the product of the comaps.

theorem MeasurableEmbedding.prodMap {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β} {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) : MeasurableEmbedding (Prod.map g f)

Prod.map of two measurable embeddings is a measurable embedding.

theorem MeasurableEmbedding.prodMk_left {α : Type u_1} [MeasurableSpace α] {β : Type u_3} {γ : Type u_4} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (x : α) {f : γ → β} (hf : MeasurableEmbedding f) : MeasurableEmbedding fun (y : γ) => (x, f y)

theorem measurableEmbedding_prodMk_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] (x : α) : MeasurableEmbedding (Prod.mk x)

theorem MeasurableEmbedding.prodMk_right {α : Type u_1} [MeasurableSpace α] {β : Type u_3} {γ : Type u_4} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : γ → β} (hf : MeasurableEmbedding f) (x : α) : MeasurableEmbedding fun (y : γ) => (f y, x)

theorem measurableEmbedding_prod_mk_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] (x : α) : MeasurableEmbedding fun (y : β) => (y, x)