English
When taking the trajectory from a to c through b, the two-step product of kernels equals the trajectory from a to c. This is a formalization of associativity in the construction of the Ionescu–Tulcea trajectory.
Русский
При прохождении траектории от a до c через b произведение ядер в двух шагах равно траектории от a до c. Это формализация ассоциативности в конструировании траектории Ionescu–Tulcea.
LaTeX
$$$ \partialTraj\,κ\,b\,c \;\circ_κ\; \partialTraj\,κ\,a\,b = \partialTraj\,κ\,a\,c \quad (a \le b \le c)$$$
Lean4
/-- Given the trajectory up to time `a`, `partialTraj κ a b` gives the distribution of
the trajectory up to time `b`. Then plugging this into `partialTraj κ b c` gives
the distribution of the trajectory up to time `c`. -/
theorem partialTraj_comp_partialTraj (hab : a ≤ b) (hbc : b ≤ c) :
partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c := by
induction c, hbc using Nat.le_induction with
| base => simp
| succ k h hk => rw [partialTraj_succ_eq_comp h, comp_assoc, hk, ← partialTraj_succ_eq_comp (hab.trans h)]
