English
Restricting the infinite product to a finite index set I yields the finite product measure: (infinitePi μ).map I.restrict = π i∈I μ_i.
Русский
Ограничение бесконечного произведения до конечного индекса I даёт конечное произведение: (infinitePi μ).map I.restrict = π_i∈I μ_i.
LaTeX
$$$$ (\mathrm{infinitePi}\,\mu)\mapsto I\!\restriction = \mathrm{Measure.pi}\bigl(\lambda i : I,\mu i\bigr). $$$$
Lean4
/-- The `projectiveFamilyContent` associated to a family of probability measures is
σ-subadditive. -/
theorem isSigmaSubadditive_piContent : (piContent μ).IsSigmaSubadditive :=
by
refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)
exact
addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders (piContent μ)
(fun s hs ↦ projectiveFamilyContent_ne_top _) (fun _ ↦ piContent_tendsto_zero μ) hf hf_Union hf'
