English
Under a decreasing sequence of cylinders with empty intersection, piContent μ (A_n) tends to 0; this is a key step toward sigma-additivity of piContent.
Русский
Для убывающей последовательности цилиндров с пустым пересечением piContent μ (A_n) стремится к 0; это ключ к сигма-аддитивности piContent.
LaTeX
$$$$\mathrm{Tendsto}\bigl(n \mapsto \piContent\mu (A_n)\bigr)\;\text{atTop}\; (\mathcal{N}\,0).$$$$
Lean4
/-- The product measure of an arbitrary family of probability measures. It is defined as the unique
extension of the function which gives to cylinders the measure given by the associated product
measure. -/
noncomputable def infinitePi : Measure (Π i, X i) :=
(piContent μ).measure isSetSemiring_measurableCylinders generateFrom_measurableCylinders.ge
(isSigmaSubadditive_piContent μ)
