English
Let μn be a probability measure on Xn and consider κi ≡ μi+1. Then the partial trajectory kernel over a,b coincides (up to an equivalence) with the product of the μi over i in Ioc(a,b), after appropriate reindexing.
Русский
Пусть μn — распределение на Xn и κi ≡ μi+1. Тогда частичное траекторное ядро на участке a..b совпадает (с учётом эквивалентности) с произведением μi по i ∈ Ioc(a,b) после подходящей переиндексации.
LaTeX
$$$$\mathrm{partialTraj}(\lambda n \mapsto \mathrm{const}_{X_{n+1}}(\mu(n+1)))\;a\;b = (\mathrm{Kernel.id} \times_κ (\mathrm{const}\_{{}}(\mathrm{Measure.pi}(\lambda i : Ioc(a,b) \mapsto \mu i))))\circ IicProdIoc(a,b).$$$$
Lean4
/-- `partialTraj κ a b` is a kernel which up to an equivalence is equal to
`Kernel.id ×ₖ (κ a ⊗ₖ ... ⊗ₖ κ (b - 1))`. This lemma therefore states that if the kernel `κ i`
is constant equal to `μ i` for all `i`, then up to an equivalence
`partialTraj κ a b = Kernel.id ×ₖ Kernel.const (⨂ μ i)`. -/
theorem partialTraj_const {a b : ℕ} :
partialTraj (fun n ↦ const _ (μ (n + 1))) a b =
(Kernel.id ×ₖ (const _ (Measure.pi (fun i : Ioc a b ↦ μ i)))).map (IicProdIoc a b) :=
by rw [partialTraj_eq_prod, partialTraj_const_restrict₂]
