π-systems generating MeasurableSpace.pi

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

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

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

theorem iUnion_le_mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.measurableCylinders α) (n : ℕ) : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ MeasureTheory.measurableCylinders α

theorem iInter_le_mem_measurableCylinders {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {s : ℕ → Set ((i : ι) → α i)} (hs : ∀ (n : ℕ), s n ∈ MeasureTheory.measurableCylinders α) (n : ℕ) : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ MeasureTheory.measurableCylinders α

def closedCompactCylinders {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → TopologicalSpace (α i)] : Set (Set ((i : ι) → α 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

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

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

@[simp]

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

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

Given a closed compact cylinder, choose a finset of variables such that it only depends on these variables.

Equations

• closedCompactCylinders.finset ht = ⋯.choose

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

Given a closed compact cylinder, choose a set depending on finitely many variables of which it is a lift.

Equations

• closedCompactCylinders.set ht = ⋯.choose

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

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

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

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

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