Approximation of product-space events by measurable cylinders #
Under a finite measure on a product space ∀ i, α i, every measurable event is approximated in
measure by a measurable cylinder over finitely many coordinates. This is Mathlib's density theorem
for a generating set ring, exists_measure_symmDiff_lt_of_generateFrom_isSetRing, applied to the
ring of measurable cylinders, which generates the product σ-algebra.
Main result #
theorem
TauCeti.MeasureTheory.exists_cylinder_measure_symmDiff_lt
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → MeasurableSpace (α i)]
{ρ : MeasureTheory.Measure ((i : ι) → α i)}
[MeasureTheory.IsFiniteMeasure ρ]
{s : Set ((i : ι) → α i)}
(hs : MeasurableSet s)
{ε : ENNReal}
(hε : 0 < ε)
:
∃ (F : Finset ι) (S : Set ((i : ↥F) → α ↑i)), MeasurableSet S ∧ ρ (symmDiff (MeasureTheory.cylinder F S) s) < ε
Every measurable event of a product space is approximated, in measure under a finite measure, by a measurable cylinder over a finite set of coordinates.