English
A version of IocProdIoc_preimage for the three-interval glued product, expressing a decomposition of the preimage into σ-products.
Русский
Версия IocProdIoc_preimage для трехинтервального зашитого произведения, выражающая разложение предобраза по σ-продуктам.
LaTeX
$$$IocProdIoc\_preimage(a,b,c)\ =\text{ (разложение по левой и правой частям) }$$$
Lean4
/-- Given a family of kernels `κ n` from `X 0 × ... × X n` to `X (n + 1)` for all `n`,
construct a kernel from `X 0 × ... × X a` to `X 0 × ... × X b` by iterating `κ`.
The idea is that the input is some trajectory up to time `a`, and the output is the distribution
of the trajectory up to time `b`. In particular if `b ≤ a`, this is just a deterministic kernel
(see `partialTraj_le`). The name `partialTraj` stands for "partial trajectory".
This kernel can be extended into a kernel with codomain `Π n, X n` via the Ionescu-Tulcea theorem.
-/
noncomputable def partialTraj (a b : ℕ) : Kernel (Π i : Iic a, X i) (Π i : Iic b, X i) :=
if h : b ≤ a then deterministic (frestrictLe₂ h) (measurable_frestrictLe₂ h)
else
@Nat.leRec a (fun b _ ↦ Kernel (Π i : Iic a, X i) (Π i : Iic b, X i)) Kernel.id
(fun k _ κ_k ↦ ((Kernel.id ×ₖ ((κ k).map (piSingleton k))) ∘ₖ κ_k).map (IicProdIoc k (k + 1))) b
(Nat.le_of_not_ge h)
