Cylinders with closed compact bases

We define the set of all cylinders with closed compact bases. Those sets play a role in the proof of Kolmogorov's extension theorem.

Main definitions

• closedCompactCylinders X: the set of all cylinders of Π i, X i based on closed compact sets.

Main statements

• mem_measurableCylinders_of_mem_closedCompactCylinders: in a topological space with second countable topology and measurable open sets, a set in closedCompactCylinders X is a measurable cylinder.

def MeasureTheory.closedCompactCylinders {ι : Type u_1} (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] : Set (Set ((i : ι) → X i))

The set of all cylinders based on closed compact sets. Note that such a set is closed, but not compact in general (for instance, the whole space is always a closed compact cylinder).

Equations

• MeasureTheory.closedCompactCylinders X = ⋃ (s : Finset ι), ⋃ (S : Set ((i : { x : ι // x ∈ s }) → X ↑i)), ⋃ (_ : IsClosed S), ⋃ (_ : IsCompact S), {MeasureTheory.cylinder s S}

theorem MeasureTheory.empty_mem_closedCompactCylinders {ι : Type u_1} (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] : ∅ ∈ closedCompactCylinders X

theorem MeasureTheory.mem_closedCompactCylinders {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] (t : Set ((i : ι) → X i)) : t ∈ closedCompactCylinders X ↔ ∃ (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → X ↑i)), IsClosed S ∧ IsCompact S ∧ t = cylinder s S

noncomputable def MeasureTheory.closedCompactCylinders.finset {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) : Finset ι

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

Equations

• MeasureTheory.closedCompactCylinders.finset ht = ⋯.choose

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

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

Equations

• MeasureTheory.closedCompactCylinders.set ht = ⋯.choose

theorem MeasureTheory.closedCompactCylinders.isClosed {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) : IsClosed (set ht)

theorem MeasureTheory.closedCompactCylinders.isCompact {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} (ht : t ∈ closedCompactCylinders X) : IsCompact (set ht)

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

theorem MeasureTheory.cylinder_mem_closedCompactCylinders {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] (s : Finset ι) (S : Set ((i : { x : ι // x ∈ s }) → X ↑i)) (hS_closed : IsClosed S) (hS_compact : IsCompact S) : cylinder s S ∈ closedCompactCylinders X

theorem MeasureTheory.mem_measurableCylinders_of_mem_closedCompactCylinders {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)} [(i : ι) → MeasurableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)] [∀ (i : ι), OpensMeasurableSpace (X i)] (ht : t ∈ closedCompactCylinders X) : t ∈ measurableCylinders X