English
Updating the finite initial segment of the trajectory distribution does not change the overall trajectory law. More precisely, if we map traj κ n x by updating the initial segment on Iic n to x, the resulting measure equals traj κ n x.
Русский
Обновление конечного начального сегмента траекторий не изменяет закон всей траектории: если применить обновляющее отображение к траекторной мере, получим ту же самую меру траектории.
LaTeX
$$$(\\operatorname{traj}_κ n x).map(\\mathrm{updateFinset}\\;\\cdot\\; (\\mathsf{Iic}\\,n)\, x) = \\operatorname{traj}_κ n x$$$
Lean4
theorem traj_map_updateFinset {n : ℕ} (x : Π i : Iic n, X i) :
(traj κ n x).map (updateFinset · (Iic n) x) = traj κ n x :=
by
nth_rw 2 [traj_eq_prod]
have : (updateFinset · _ x) = IicProdIoi n ∘ (Prod.mk x) ∘ (Set.Ioi n).restrict := by ext;
simp [IicProdIoi, updateFinset]
rw [this, ← Function.comp_assoc, ← Measure.map_map, ← Measure.map_map, map_apply, prod_apply, map_apply, id_apply,
Measure.dirac_prod]
all_goals fun_prop
