English
With the finite kernel assumption, the partialTraj a b is equivalent to a product form involving an identity and a restricted partial trajectory, transported by IicProdIoc. This allows to pass from the joint trajectory to marginal pieces.
Русский
При предположении о конечности ядер partialTraj a b эквивалентна формe произведения, включающем тождественный компонент и ограниченную частичную траекторию, перенесенную через IicProdIoc. Это позволяет перейти от совместной траектории к маргинальным частям.
LaTeX
$$$ \partialTraj\,κ\,a\,b = (\mathrm{Id} \times\_k (\partialTraj\,κ\,a\,b).map(\mathrm{restrict}_2\ Ioc\_subset\_Iic\_self)).map(IicProdIoc\,a\,b)$$$
Lean4
/-- If we restrict the distribution of the trajectory up to time `c` to times `≤ b` we get
the trajectory up to time `b`. -/
theorem partialTraj_map_frestrictLe₂ (a : ℕ) (hbc : b ≤ c) :
(partialTraj κ a c).map (frestrictLe₂ hbc) = partialTraj κ a b := by
induction c, hbc using Nat.le_induction with
| base => exact map_id ..
| succ k h
hk =>
rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right, partialTraj_succ_map_frestrictLe₂]
all_goals fun_prop
