English
If a and b relate by inclusion, the equality of the finite product measures under Iic and Ioc holds, yielding the same π-measure on Iic b.
Русский
Если a и b взаимно включаются, то равенство произведений мер под Iic и Ioc сохраняется, давая ту же π-меру на 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 : Iic b) → Measure (X i)` be a family of measures. Up to an equivalence,
`(⨂ i : Iic a, μ i) ⊗ (⨂ i : Ioc a b, μ i) = ⨂ i : Iic b, μ i`, where `⊗` denotes the
product of measures. -/
theorem pi_prod_map_IicProdIoc {a b : ℕ} :
((Measure.pi (fun i : Iic a ↦ μ i)).prod (Measure.pi (fun i : Ioc a b ↦ μ i))).map (IicProdIoc a b) =
Measure.pi (fun i : Iic b ↦ μ i) :=
by
obtain hab | hba := le_total a b
· refine (Measure.pi_eq fun s ms ↦ ?_).symm
simp_rw [Measure.map_apply measurable_IicProdIoc (.univ_pi ms), IicProdIoc_preimage hab, Measure.prod_prod,
Measure.pi_pi, prod_eq_prod_extend]
nth_rw 1 [Eq.comm, ← Iic_union_Ioc_eq_Iic hab, prod_union (Iic_disjoint_Ioc le_rfl)]
congr 1 <;> refine prod_congr rfl fun x hx ↦ ?_
· rw [Function.extend_val_apply hx, Function.extend_val_apply (Iic_subset_Iic.2 hab hx), frestrictLe₂, restrict₂]
· rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Iic_self hx), restrict₂]
· rw [IicProdIoc_le hba, ← Measure.map_map, ← Measure.fst, Measure.fst_prod]
· exact isProjectiveMeasureFamily_pi μ (Iic a) (Iic b) (Iic_subset_Iic.2 hba) |>.symm
all_goals fun_prop
