π-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 setS : Set (∀ i : s, α i)
wheres
is aFinset
squareCylinders C
withC : ∀ i, Set (Set (α i))
: set of all square cylinders such that for alli
in the finset defining the box, the projection toα i
belongs toC i
. The main application of this is withC 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 σ-algebragenerateFrom_measurableCylinders
: cylinders formed from measurable sets generate the product σ-algebra
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}
Instances For
The square cylinders formed from measurable sets generate the product σ-algebra.
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 = s.restrict ⁻¹' S
Instances For
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}
Instances For
A finset s
such that t = cylinder s S
. S
is given by measurableCylinders.set
.
Equations
- MeasureTheory.measurableCylinders.finset ht = ⋯.choose
Instances For
A set S
such that t = cylinder s S
. s
is given by measurableCylinders.finset
.
Equations
- MeasureTheory.measurableCylinders.set ht = ⋯.choose
Instances For
The measurable cylinders generate the product σ-algebra.