English
A variant of eq_traj' that incorporates the universal quantifier over a fixed a and n and states that the trajectory η must coincide with traj κ a if its projections agree with partialTraj for all b ≥ n.
Русский
Вариант eq_traj', который утверждает, что если проекции η совпадают с partialTraj для всех b ≥ n, то η совпадает с traj κ a.
LaTeX
$$$\\forall a\\, n\\,\\eta,\\ (\\forall b \\ge n,\\ \\eta.map(\\mathrm{frestrictLe}\\ b) = partialTraj\\ κ\\ a\\ b) \\Rightarrow η = traj\\ κ\\ a$$$
Lean4
/-- *Ionescu-Tulcea Theorem* : Given a family of kernels `κ n` taking variables in `Iic n` with
value in `X (n + 1)`, the kernel `traj κ a` takes a variable `x` depending on the
variables `i ≤ a` and associates to it a kernel on trajectories depending on all variables,
where the entries with index `≤ a` are those of `x`, and then one follows iteratively the
kernels `κ a`, then `κ (a + 1)`, and so on.
The fact that such a kernel exists on infinite trajectories is not obvious, and is the content of
the Ionescu-Tulcea theorem. -/
noncomputable def traj (a : ℕ) : Kernel (Π i : Iic a, X i) (Π n, X n)
where
toFun := trajFun κ a
measurable' := measurable_trajFun a
