English
Let κ be a family of kernels indexed by natural numbers. For any a ∈ N, the distribution of the trajectory from time a to a+1 can be written as a product of the identity on the past up to time a and the transition κ_a from time a to a+1, then transported to the interval up to a+1 via the canonical projection. In particular, the a-th step is independent from the past and governed by κ_a.
Русский
Пусть κ — семействоKernel, индексируемое по натуральным чисам. Для любого a ∈ N распределение траектории от времени a до a+1 записывается как произведение тождественного распределения по прошлому до момента a и перехода κ_a от времени a к a+1, затем перенесенное на интервал до a+1 через каноническое отображение. В частности, шаг в момент a независимо от прошлого и задается κ_a.
LaTeX
$$$ \partialTraj\,κ\,a\,(a+1) = (\mathrm{KerId} \;\times\_k ((κ\,a).map(\pi_{\{a\}}))).map(IicProdIoc\,a\,(a+1))$$$
Lean4
theorem partialTraj_succ_self (a : ℕ) :
partialTraj κ a (a + 1) = (Kernel.id ×ₖ ((κ a).map (piSingleton a))).map (IicProdIoc a (a + 1)) := by
rw [partialTraj_succ_of_le le_rfl, partialTraj_self, comp_id]
