English
The infinite product measure is the projective limit of the finite marginals: IsProjectiveLimit (infinitePi μ) (I ↦ π μ_I).
Русский
Бесконечное произведение меры является проективным пределом конечных маргиналов: IsProjectiveLimit (infinitePi μ) (I ↦ π μ_I).
LaTeX
$$$$IsProjectiveLimit\bigl(\mathrm{infinitePi}\,\mu\bigr)\;\bigl(\lambda I. \mathrm{Measure.pi}(\lambda i:\; I \mapsto \mu i)\bigr).$$$$
Lean4
/-- The product measure is the projective limit of the partial product measures. This ensures
uniqueness and expresses the value of the product measure applied to cylinders. -/
theorem isProjectiveLimit_infinitePi :
IsProjectiveLimit (infinitePi μ) (fun I : Finset ι ↦ (Measure.pi (fun i : I ↦ μ i))) :=
by
intro I
ext s hs
rw [map_apply (measurable_restrict I) hs, infinitePi, AddContent.measure_eq, ← cylinder, piContent_cylinder μ hs]
· exact generateFrom_measurableCylinders.symm
· exact cylinder_mem_measurableCylinders _ _ hs
