The product sigma algebra #
This file talks about the measurability of operations on binary functions.
theorem
generateFrom_prod_eq
{α : Type u_4}
{β : Type u_5}
{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
MeasurableEmbedding.prod_mk
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
{δ : Type u_7}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ}
{f : α → β}
{g : γ → δ}
(hg : MeasurableEmbedding g)
(hf : MeasurableEmbedding f)
:
MeasurableEmbedding fun (x : γ × α) => (g x.1, f x.2)
theorem
MeasurableEmbedding.prod_mk_left
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_4}
{γ : Type u_5}
[MeasurableSingletonClass α]
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(x : α)
{f : γ → β}
(hf : MeasurableEmbedding f)
:
MeasurableEmbedding fun (y : γ) => (x, f y)
theorem
measurableEmbedding_prod_mk_left
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
(x : α)
:
theorem
MeasurableEmbedding.prod_mk_right
{α : Type u_1}
[MeasurableSpace α]
{β : Type u_4}
{γ : Type u_5}
[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)