π-systems of cylinders and square cylinders

The instance MeasurableSpace.pi on ∀ i, α i, where each α i has a MeasurableSpace m i, is defined as ⨆ i, (m i).comap (fun a => a i). That is, a function g : β → ∀ i, α i is measurable iff for all i, the function b ↦ g b i is measurable.

We define two π-systems generating MeasurableSpace.pi, cylinders and square cylinders.

Main definitions

Given a finite set s of indices, a cylinder is the product of a set of ∀ i : s, α i and of univ on the other indices. A square cylinder is a cylinder for which the set on ∀ i : s, α i is a product set.

• cylinder s S: cylinder with base set S : Set (∀ i : s, α i) where s is a Finset
• squareCylinders C with C : ∀ i, Set (Set (α i)): set of all square cylinders such that for all i in the finset defining the box, the projection to α i belongs to C i. The main application of this is with C i = {s : Set (α i) | MeasurableSet s}.
• measurableCylinders: set of all cylinders with measurable base sets.

Main statements

• generateFrom_squareCylinders: square cylinders formed from measurable sets generate the product σ-algebra
• generateFrom_measurableCylinders: cylinders formed from measurable sets generate the product σ-algebra

def MeasureTheory.squareCylinders {ι : Type u_1} {α : ι → Type u_2} (C : (i : ι) → Set (Set (α i))) : Set (Set ((i : ι) → α i))

Given a finite set s of indices, a square cylinder is the product of a set S of ∀ i : s, α i and of univ on the other indices. The set S is a product of sets t i such that for all i : s, t i ∈ C i. squareCylinders is the set of all such squareCylinders.

Equations

• MeasureTheory.squareCylinders C = {S : Set ((i : ι) → α i) | ∃ (s : Finset ι), ∃ t ∈ Set.univ.pi C, S = (↑s).pi t}

theorem MeasureTheory.squareCylinders_eq_iUnion_image {ι : Type u_2} {α : ι → Type u_1} (C : (i : ι) → Set (Set (α i))) : MeasureTheory.squareCylinders C = ⋃ (s : Finset ι), (fun (t : (i : ι) → Set (α i)) => (↑s).pi t) '' Set.univ.pi C

theorem MeasureTheory.isPiSystem_squareCylinders {ι : Type u_2} {α : ι → Type u_1} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsPiSystem (C i)) (hC_univ : ∀ (i : ι), Set.univ ∈ C i) : IsPiSystem (MeasureTheory.squareCylinders C)

theorem MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton {ι : Type u_2} (α : ι → Type u_1) [m : (i : ι) → MeasurableSpace (α i)] (i : ι) : MeasurableSpace.comap (Function.eval i) (m i) ≤ MeasurableSpace.generateFrom ((fun (t : (i : ι) → Set (α i)) => {i}.pi t) '' Set.univ.pi fun (i : ι) => {s : Set (α i) | MeasurableSet s})

theorem MeasureTheory.generateFrom_squareCylinders {ι : Type u_2} {α : ι → Type u_1} [(i : ι) → MeasurableSpace (α i)] : MeasurableSpace.generateFrom (MeasureTheory.squareCylinders fun (i : ι) => {s : Set (α i) | MeasurableSet s}) = MeasurableSpace.pi

The square cylinders formed from measurable sets generate the product σ-algebra.

def MeasureTheory.cylinder {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)) : Set ((i : ι) → α i)

Given a finite set s of indices, a cylinder is the preimage of a set S of ∀ i : s, α i by the projection from ∀ i, α i to ∀ i : s, α i.

Equations

• MeasureTheory.cylinder s S = (fun (f : (i : ι) → α i) (i : { x : ι // x ∈ s }) => f ↑i) ⁻¹' S

@[simp]

theorem MeasureTheory.mem_cylinder {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)) (f : (i : ι) → α i) : f ∈ MeasureTheory.cylinder s S ↔ (fun (i : { x : ι // x ∈ s }) => f ↑i) ∈ S

@[simp]

theorem MeasureTheory.cylinder_empty {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) : MeasureTheory.cylinder s ∅ = ∅

@[simp]

theorem MeasureTheory.cylinder_univ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) : MeasureTheory.cylinder s Set.univ = Set.univ

@[simp]

theorem MeasureTheory.cylinder_eq_empty_iff {ι : Type u_1} {α : ι → Type u_2} [h_nonempty : Nonempty ((i : ι) → α i)] (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)) : MeasureTheory.cylinder s S = ∅ ↔ S = ∅

theorem MeasureTheory.inter_cylinder {ι : Type u_1} {α : ι → Type u_2} (s₁ : Finset ι) (s₂ : Finset ι) (S₁ : Set ((i : { x : ι // x ∈ s₁ }) → α ↑i)) (S₂ : Set ((i : { x : ι // x ∈ s₂ }) → α ↑i)) [DecidableEq ι] : MeasureTheory.cylinder s₁ S₁ ∩ MeasureTheory.cylinder s₂ S₂ = MeasureTheory.cylinder (s₁ ∪ s₂) ((fun (f : (i : { x : ι // x ∈ s₁ ∪ s₂ }) → α ↑i) (j : { x : ι // x ∈ s₁ }) => f ⟨↑j, ⋯⟩) ⁻¹' S₁ ∩ (fun (f : (i : { x : ι // x ∈ s₁ ∪ s₂ }) → α ↑i) (j : { x : ι // x ∈ s₂ }) => f ⟨↑j, ⋯⟩) ⁻¹' S₂)

theorem MeasureTheory.inter_cylinder_same {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S₁ : Set ((i : { x : ι // x ∈ s }) → α ↑i)) (S₂ : Set ((i : { x : ι // x ∈ s }) → α ↑i)) : MeasureTheory.cylinder s S₁ ∩ MeasureTheory.cylinder s S₂ = MeasureTheory.cylinder s (S₁ ∩ S₂)

theorem MeasureTheory.union_cylinder {ι : Type u_1} {α : ι → Type u_2} (s₁ : Finset ι) (s₂ : Finset ι) (S₁ : Set ((i : { x : ι // x ∈ s₁ }) → α ↑i)) (S₂ : Set ((i : { x : ι // x ∈ s₂ }) → α ↑i)) [DecidableEq ι] : MeasureTheory.cylinder s₁ S₁ ∪ MeasureTheory.cylinder s₂ S₂ = MeasureTheory.cylinder (s₁ ∪ s₂) ((fun (f : (i : { x : ι // x ∈ s₁ ∪ s₂ }) → α ↑i) (j : { x : ι // x ∈ s₁ }) => f ⟨↑j, ⋯⟩) ⁻¹' S₁ ∪ (fun (f : (i : { x : ι // x ∈ s₁ ∪ s₂ }) → α ↑i) (j : { x : ι // x ∈ s₂ }) => f ⟨↑j, ⋯⟩) ⁻¹' S₂)

theorem MeasureTheory.union_cylinder_same {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S₁ : Set ((i : { x : ι // x ∈ s }) → α ↑i)) (S₂ : Set ((i : { x : ι // x ∈ s }) → α ↑i)) : MeasureTheory.cylinder s S₁ ∪ MeasureTheory.cylinder s S₂ = MeasureTheory.cylinder s (S₁ ∪ S₂)

theorem MeasureTheory.compl_cylinder {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)) : (MeasureTheory.cylinder s S)ᶜ = MeasureTheory.cylinder s Sᶜ

theorem MeasureTheory.diff_cylinder_same {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)) (T : Set ((i : { x : ι // x ∈ s }) → α ↑i)) : MeasureTheory.cylinder s S \ MeasureTheory.cylinder s T = MeasureTheory.cylinder s (S \ T)

theorem MeasureTheory.eq_of_cylinder_eq_of_subset {ι : Type u_1} {α : ι → Type u_2} [h_nonempty : Nonempty ((i : ι) → α i)] {I : Finset ι} {J : Finset ι} {S : Set ((i : { x : ι // x ∈ I }) → α ↑i)} {T : Set ((i : { x : ι // x ∈ J }) → α ↑i)} (h_eq : MeasureTheory.cylinder I S = MeasureTheory.cylinder J T) (hJI : J ⊆ I) : S = (fun (f : (i : { x : ι // x ∈ I }) → α ↑i) (j : { x : ι // x ∈ J }) => f ⟨↑j, ⋯⟩) ⁻¹' T

theorem MeasureTheory.cylinder_eq_cylinder_union {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] (I : Finset ι) (S : Set ((i : { x : ι // x ∈ I }) → α ↑i)) (J : Finset ι) : MeasureTheory.cylinder I S = MeasureTheory.cylinder (I ∪ J) ((fun (f : (i : { x : ι // x ∈ I ∪ J }) → α ↑i) (j : { x : ι // x ∈ I }) => f ⟨↑j, ⋯⟩) ⁻¹' S)

theorem MeasureTheory.disjoint_cylinder_iff {ι : Type u_1} {α : ι → Type u_2} [Nonempty ((i : ι) → α i)] {s : Finset ι} {t : Finset ι} {S : Set ((i : { x : ι // x ∈ s }) → α ↑i)} {T : Set ((i : { x : ι // x ∈ t }) → α ↑i)} [DecidableEq ι] : Disjoint (MeasureTheory.cylinder s S) (MeasureTheory.cylinder t T) ↔ Disjoint ((fun (f : (i : { x : ι // x ∈ s ∪ t }) → α ↑i) (j : { x : ι // x ∈ s }) => f ⟨↑j, ⋯⟩) ⁻¹' S) ((fun (f : (i : { x : ι // x ∈ s ∪ t }) → α ↑i) (j : { x : ι // x ∈ t }) => f ⟨↑j, ⋯⟩) ⁻¹' T)

theorem MeasureTheory.IsClosed.cylinder {ι : Type u_2} {α : ι → Type u_1} [(i : ι) → TopologicalSpace (α i)] (s : Finset ι) {S : Set ((i : { x : ι // x ∈ s }) → α ↑i)} (hs : IsClosed S) : IsClosed (MeasureTheory.cylinder s S)

theorem MeasurableSet.cylinder {ι : Type u_2} {α : ι → Type u_1} [(i : ι) → MeasurableSpace (α i)] (s : Finset ι) {S : Set ((i : { x : ι // x ∈ s }) → α ↑i)} (hS : MeasurableSet S) : MeasurableSet (MeasureTheory.cylinder s S)

def MeasureTheory.measurableCylinders {ι : Type u_2} (α : ι → Type u_1) [(i : ι) → MeasurableSpace (α i)] : Set (Set ((i : ι) → α i))

Given a finite set s of indices, a cylinder is the preimage of a set S of ∀ i : s, α i by the projection from ∀ i, α i to ∀ i : s, α i. measurableCylinders is the set of all cylinders with measurable base S.

Equations

• MeasureTheory.measurableCylinders α = ⋃ (s : Finset ι), ⋃ (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)), ⋃ (_ : MeasurableSet S), {MeasureTheory.cylinder s S}

theorem MeasureTheory.empty_mem_measurableCylinders {ι : Type u_2} (α : ι → Type u_1) [(i : ι) → MeasurableSpace (α i)] : ∅ ∈ MeasureTheory.measurableCylinders α

@[simp]

theorem MeasureTheory.mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (t : Set ((i : ι) → α i)) : t ∈ MeasureTheory.measurableCylinders α ↔ ∃ (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)), MeasurableSet S ∧ t = MeasureTheory.cylinder s S

noncomputable def MeasureTheory.measurableCylinders.finset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t ∈ MeasureTheory.measurableCylinders α) : Finset ι

A finset s such that t = cylinder s S. S is given by measurableCylinders.set.

Equations

• MeasureTheory.measurableCylinders.finset ht = ⋯.choose

def MeasureTheory.measurableCylinders.set {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t ∈ MeasureTheory.measurableCylinders α) : Set ((i : { x : ι // x ∈ MeasureTheory.measurableCylinders.finset ht }) → α ↑i)

A set S such that t = cylinder s S. s is given by measurableCylinders.finset.

Equations

• MeasureTheory.measurableCylinders.set ht = ⋯.choose

theorem MeasureTheory.measurableCylinders.measurableSet {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t ∈ MeasureTheory.measurableCylinders α) : MeasurableSet (MeasureTheory.measurableCylinders.set ht)

theorem MeasureTheory.measurableCylinders.eq_cylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t ∈ MeasureTheory.measurableCylinders α) : t = MeasureTheory.cylinder (MeasureTheory.measurableCylinders.finset ht) (MeasureTheory.measurableCylinders.set ht)

theorem MeasureTheory.cylinder_mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → α ↑i)) (hS : MeasurableSet S) : MeasureTheory.cylinder s S ∈ MeasureTheory.measurableCylinders α

theorem MeasureTheory.inter_mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : s ∈ MeasureTheory.measurableCylinders α) (ht : t ∈ MeasureTheory.measurableCylinders α) : s ∩ t ∈ MeasureTheory.measurableCylinders α

theorem MeasureTheory.isPiSystem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] : IsPiSystem (MeasureTheory.measurableCylinders α)

theorem MeasureTheory.compl_mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} (hs : s ∈ MeasureTheory.measurableCylinders α) : sᶜ ∈ MeasureTheory.measurableCylinders α

theorem MeasureTheory.univ_mem_measurableCylinders {ι : Type u_2} (α : ι → Type u_1) [(i : ι) → MeasurableSpace (α i)] : Set.univ ∈ MeasureTheory.measurableCylinders α

theorem MeasureTheory.union_mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : s ∈ MeasureTheory.measurableCylinders α) (ht : t ∈ MeasureTheory.measurableCylinders α) : s ∪ t ∈ MeasureTheory.measurableCylinders α

theorem MeasureTheory.diff_mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : s ∈ MeasureTheory.measurableCylinders α) (ht : t ∈ MeasureTheory.measurableCylinders α) : s \ t ∈ MeasureTheory.measurableCylinders α

theorem MeasureTheory.generateFrom_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] : MeasurableSpace.generateFrom (MeasureTheory.measurableCylinders α) = MeasurableSpace.pi

The measurable cylinders generate the product σ-algebra.