English
Let a ≤ b ≤ c. The product of π-measures on Ioc intervals Ioc a b and Ioc b c, mapped by IocProdIoc, equals the π-measure on Ioc a c.
Русский
Пусть a ≤ b ≤ c. Произведение мер π на интервалах Ioc a b и Ioc b c, отображённое через IocProdIoc, равно π-мера на Ioc a c.
LaTeX
$$$((\text{Measure.pi } (fun i:\, Ioc a b ↦ μ i)).prod (\text{Measure.pi } (fun i:\, Ioc b c ↦ μ i))).map (IocProdIoc a b c) = \text{Measure.pi } (fun i:\, Ioc a c ↦ μ i)$$$
Lean4
/-- Consider a family of probability measures. You can take their products for any finite
subfamily. This gives a projective family of measures. -/
theorem isProjectiveMeasureFamily_pi : IsProjectiveMeasureFamily (fun I : Finset ι ↦ (Measure.pi (fun i : I ↦ μ i))) :=
by
refine fun I J hJI ↦ Measure.pi_eq (fun s ms ↦ ?_)
classical
simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI, Measure.pi_pi,
prod_eq_prod_extend]
refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
· rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
· rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]
