English
For a ≤ b ≤ c, the mapping sends the product of π-measures on Iic a and Ioc a b to the product on Iic b, mirroring the associativity of infinite products.
Русский
При a ≤ b ≤ c отображение переводит произведение π-мера на 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
/-- Let `μ : (i : Ioc a c) → Measure (X i)` be a family of measures. Up to an equivalence,
`(⨂ i : Ioc a b, μ i) ⊗ (⨂ i : Ioc b c, μ i) = ⨂ i : Ioc a c, μ i`, where `⊗` denotes the
product of measures. -/
theorem pi_prod_map_IocProdIoc {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) :
((Measure.pi (fun i : Ioc a b ↦ μ i)).prod (Measure.pi (fun i : Ioc b c ↦ μ i))).map (IocProdIoc a b c) =
Measure.pi (fun i : Ioc a c ↦ μ i) :=
by
refine (Measure.pi_eq fun s ms ↦ ?_).symm
simp_rw [Measure.map_apply measurable_IocProdIoc (.univ_pi ms), IocProdIoc_preimage hab hbc, Measure.prod_prod,
Measure.pi_pi, prod_eq_prod_extend]
nth_rw 1 [Eq.comm, ← Ioc_union_Ioc_eq_Ioc hab hbc, prod_union (Ioc_disjoint_Ioc_of_le le_rfl)]
congr 1 <;> refine prod_congr rfl fun x hx ↦ ?_
· rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_right hbc hx), restrict₂]
· rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_left hab hx), restrict₂]
