English
For intervals Iic a and Ioc a b, the combined product measure, under the appropriate embeddings and equivalences, equals the π-measure on Iic b.
Русский
Для интервалов Iic a и Ioc a b произведение мер совпадает с π-мерой на Iic b под соответствующими вложениями.
LaTeX
$$$((\text{Measure.pi } (fun i:\, Iic a ↦ μ i)).prod (\text{Measure.pi } (fun i:\, Ioc a b ↦ μ i))).map (IicProdIoc a b) = \text{Measure.pi } (fun i:\, Iic b ↦ μ i)$$$
Lean4
/-- Consider a family of probability measures. You can take their products for any finite
subfamily. This gives an additive content on the measurable cylinders. -/
noncomputable def piContent : AddContent (measurableCylinders X) :=
projectiveFamilyContent (isProjectiveMeasureFamily_pi μ)
