English
Let κ be a Markov kernel sequence and let traj κ n denote the distribution of the trajectory up to time n. For any a ≤ b, the distribution up to time a can be obtained by first evolving to time b via the partial trajectory and then applying the trajectory map for time b. In symbols, traj κ b composed with partialTraj κ a b equals traj κ a.
Русский
Пусть κ — последовательность марковских ядер, и пусть traj κ n обозначает распределение траектории до времени n. Для любого a ≤ b распределение до времени a можно получить, сначала пройдя до времени b с помощью partialTraj κ a b, затем применив traj κ b. Формально: traj κ b ∘ₖ partialTraj κ a b = traj κ a.
LaTeX
$$$\\ (\\operatorname{traj}_\\kappa b) \\circ_\\kappa (\\partial_\\kappa a b) = \\operatorname{traj}_\\kappa a \\; (a \\le b) $$$
Lean4
/-- Given the distribution up to tome `a`, `partialTraj κ a b` gives the distribution
of the trajectory up to time `b`, and composing this with `traj κ b` gives the distribution
of the whole trajectory. -/
theorem traj_comp_partialTraj {a b : ℕ} (hab : a ≤ b) : (traj κ b) ∘ₖ (partialTraj κ a b) = traj κ a :=
by
refine eq_traj _ _ fun n ↦ ?_
rw [map_comp, traj_map_frestrictLe, partialTraj_comp_partialTraj' _ hab]
