English
Fix a and n. If η is a kernel with the property that for all b ≥ n, η.map (frestrictLe b) = partialTraj κ a b, then η = traj κ a.
Русский
Зафиксируем a и n. Если η — ядро с тем свойством, что для всех b ≥ n имеет η.map (frestrictLe b) = partialTraj κ a b, тогда η = traj κ a.
LaTeX
$$$\\bigl(\\forall b:\\mathbb{N}, b \\ge n \\Rightarrow η.map(\\mathrm{frestrictLe}\\ b) = partialTraj\\ κ\\ a\\ b\\bigr) \\Rightarrow η = traj\\ κ\\ a$$$
Lean4
/-- This function is the kernel given by the Ionescu-Tulcea theorem. It is shown below that it
is measurable and turned into a true kernel in `Kernel.traj`. -/
noncomputable def trajFun (a : ℕ) (x₀ : Π i : Iic a, X i) : Measure (Π n, X n) :=
(trajContent κ x₀).measure isSetSemiring_measurableCylinders generateFrom_measurableCylinders.ge
(isSigmaSubadditive_trajContent κ x₀)
