π-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.
• cylinderEvents Δ: The σ-algebra of cylinder events on Δ. It is the smallest σ-algebra making the projections on the i-th coordinate continuous for all i ∈ Δ.

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.

theorem MeasureTheory.squareCylinders_eq_iUnion_image {ι : Type u_2} {α : ι → Type u_1} (C : (i : ι) → Set (Set (α i))) : 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 (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 (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.

@[simp]

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

@[simp]

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

@[simp]

theorem MeasureTheory.cylinder_univ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) : 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)) : cylinder s S = ∅ ↔ S = ∅

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

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

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

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

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

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

theorem MeasureTheory.eq_of_cylinder_eq_of_subset {ι : Type u_1} {α : ι → Type u_2} [h_nonempty : Nonempty ((i : ι) → α i)] {I J : Finset ι} {S : Set ((i : { x : ι // x ∈ I }) → α ↑i)} {T : Set ((i : { x : ι // x ∈ J }) → α ↑i)} (h_eq : cylinder I S = cylinder J T) (hJI : J ⊆ I) : S = Finset.restrict₂ hJI ⁻¹' 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 ι) : cylinder I S = cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)

theorem MeasureTheory.disjoint_cylinder_iff {ι : Type u_1} {α : ι → Type u_2} [Nonempty ((i : ι) → α i)] {s t : Finset ι} {S : Set ((i : { x : ι // x ∈ s }) → α ↑i)} {T : Set ((i : { x : ι // x ∈ t }) → α ↑i)} [DecidableEq ι] : Disjoint (cylinder s S) (cylinder t T) ↔ Disjoint (Finset.restrict₂ ⋯ ⁻¹' S) (Finset.restrict₂ ⋯ ⁻¹' 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)

theorem MeasureTheory.dependsOn_cylinder_indicator_const {ι : Type u_2} {α : ι → Type u_3} {M : Type u_1} [Zero M] {I : Finset ι} (S : Set ((i : { x : ι // x ∈ I }) → α ↑i)) (c : M) : DependsOn ((cylinder I S).indicator fun (x : (i : ι) → α i) => c) ↑I

The indicator of a cylinder only depends on the variables whose the cylinder depends on.

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.

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

@[simp]

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

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

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

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

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

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

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

theorem MeasureTheory.measurableCylinders.eq_cylinder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {t : Set ((i : ι) → α i)} (ht : t ∈ measurableCylinders α) : t = cylinder (finset ht) (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) : cylinder s S ∈ measurableCylinders α

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

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

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

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

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

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

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

The measurable cylinders generate the product σ-algebra.

theorem MeasureTheory.measurableCylinders_nat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] : measurableCylinders X = ⋃ (a : ℕ), ⋃ (S : Set ((i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i)), ⋃ (_ : MeasurableSet S), {cylinder (Finset.Iic a) S}

The cylinders of a product space indexed by ℕ can be seen as depending on the first coordinates.

Cylinder events as a sigma-algebra

def MeasureTheory.cylinderEvents {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] (Δ : Set ι) : MeasurableSpace ((i : ι) → X i)

The σ-algebra of cylinder events on Δ. It is the smallest σ-algebra making the projections on the i-th coordinate measurable for all i ∈ Δ.

@[simp]

theorem MeasureTheory.cylinderEvents_univ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] : cylinderEvents Set.univ = MeasurableSpace.pi

theorem MeasureTheory.cylinderEvents_mono {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ₁ Δ₂ : Set ι} (h : Δ₁ ⊆ Δ₂) : cylinderEvents Δ₁ ≤ cylinderEvents Δ₂

theorem MeasureTheory.cylinderEvents_le_pi {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} : cylinderEvents Δ ≤ MeasurableSpace.pi

theorem MeasureTheory.measurable_cylinderEvents_iff {α : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {mα : MeasurableSpace α} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {g : α → (i : ι) → X i} : Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable fun (a : α) => g a i

theorem MeasureTheory.measurable_cylinderEvent_apply {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {i : ι} (hi : i ∈ Δ) : Measurable fun (f : (i : ι) → X i) => f i

theorem MeasureTheory.Measurable.eval_cylinderEvents {α : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {mα : MeasurableSpace α} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {i : ι} {g : α → (i : ι) → X i} (hi : i ∈ Δ) (hg : Measurable g) : Measurable fun (a : α) => g a i

theorem MeasureTheory.measurable_cylinderEvents_lambda {α : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {mα : MeasurableSpace α} [m : (i : ι) → MeasurableSpace (X i)] (f : α → (i : ι) → X i) (hf : ∀ (i : ι), Measurable fun (a : α) => f a i) : Measurable f

theorem MeasureTheory.measurable_update_cylinderEvents' {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {i : ι} [DecidableEq ι] : Measurable fun (p : ((i : ι) → X i) × X i) => Function.update p.1 i p.2

The function (f, x) ↦ update f a x : (Π a, X a) × X a → Π a, X a is measurable.

theorem MeasureTheory.measurable_uniqueElim_cylinderEvents {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] [Unique ι] : Measurable uniqueElim

theorem MeasureTheory.measurable_update_cylinderEvents {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} (f : (a : ι) → X a) {a : ι} [DecidableEq ι] : Measurable (Function.update f a)

The function update f a : X a → Π a, X a is always measurable. This doesn't require f to be measurable. This should not be confused with the statement that update f a x is measurable.

theorem MeasureTheory.measurable_update_cylinderEvents_left {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {a : ι} [DecidableEq ι] {x : X a} : Measurable fun (x_1 : (i : ι) → X i) => Function.update x_1 a x

theorem MeasureTheory.measurable_restrict_cylinderEvents {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] (Δ : Set ι) : Measurable Δ.restrict