English
There is a canonical equivalence expressing traj κ a as the product of a deterministic kernel and a conditional part of the trajectory, followed by a measurable reindexing. This shows traj κ a is, up to isomorphism, a product of a fixed component and the residual trajectory.
Русский
Существует каноническое эквивалентное разложение траектории: траектория κ до времени a равна произведению детерминированного ядра и условной части траектории, после чего применяется подходящее отображение. Это показывает, что траектория κ a ≈ детерминированное ядро × остаточная траектория.
LaTeX
$$$\\operatorname{traj}_\\kappa a = (\\operatorname{id} \\times_\\kappa (\\operatorname{traj}_\\kappa a).map(\\mathbf{1}_{(a,\\infty)}) \\big)^{\\!\\sim} \\! \\mathrm{(IicProdIoi a)}$$$
Lean4
/-- This theorem shows that `traj κ n` is, up to an equivalence, the product of
a deterministic kernel with another kernel. This is an intermediate result to compute integrals
with respect to this kernel. -/
theorem traj_eq_prod (a : ℕ) : traj κ a = (Kernel.id ×ₖ (traj κ a).map (Set.Ioi a).restrict).map (IicProdIoi a) :=
by
refine (eq_traj' _ (a + 1) _ fun b hb ↦ ?_).symm
rw [← map_comp_right]
conv_lhs => enter [2]; change (IicProdIoc a b) ∘ (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).1⟩))
· rw [map_comp_right, ← map_prod_map, ← map_comp_right]
· conv_lhs => enter [1, 2, 2]; change (Ioc a b).restrict
rw [← restrict₂_comp_restrict Ioc_subset_Iic_self, ← frestrictLe, map_comp_right, traj_map_frestrictLe, map_id, ←
partialTraj_eq_prod]
all_goals fun_prop
all_goals fun_prop
all_goals fun_prop
