English
Under the finiteness hypothesis on the kernels, the partial trajectory from a to b can be written as a product of an identity on the first coordinate and the map of the remaining partial trajectory through an Ioc–Iic product projection. This isolates the initial component from the rest of the trajectory.
Русский
При условии конечности ядер частичная траектория от a до b может быть записана как произведение тождественного распределения на первой координате и отображения остаточной траектории через проекцию Ioc–Iic. Это выделяет начальную часть траектории.
LaTeX
$$$ \partialTraj\,κ\,a\,b = (\mathrm{Id} \times\_k (\partialTraj\,κ\,a\,b).map(\mathrm{restrict}_2\ Ioc\_subset\_Iic\_self)).map(IicProdIoc\,a\,b)$$$
Lean4
/-- This is a technical lemma saying that `partialTraj κ a b` consists of two independent parts, the
first one being the identity. It allows to compute integrals. -/
theorem partialTraj_eq_prod [∀ n, IsSFiniteKernel (κ n)] (a b : ℕ) :
partialTraj κ a b = (Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ Ioc_subset_Iic_self)).map (IicProdIoc a b) :=
by
obtain hba | hab := le_total b a
· rw [partialTraj_le hba, IicProdIoc_le hba, map_comp_right, ← fst_eq, deterministic_map, fst_prod, id_map]
all_goals fun_prop
induction b, hab using Nat.le_induction with
| base =>
ext1 x
rw [partialTraj_self, id_map, map_apply, prod_apply, IicProdIoc_self, ← Measure.fst, Measure.fst_prod]
all_goals fun_prop
| succ k h
hk =>
have :
(IicProdIoc (X := X) k (k + 1)) ∘ (Prod.map (IicProdIoc a k) id) =
(IicProdIoc (h.trans k.le_succ) ∘ (Prod.map id (IocProdIoc a k (k + 1)))) ∘ prodAssoc :=
by
ext x i
simp only [IicProdIoc_def, MeasurableEquiv.IicProdIoc, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk,
Function.comp_apply, Prod.map_fst, Prod.map_snd, id_eq, Nat.succ_eq_add_one, IocProdIoc]
split_ifs <;> try rfl
omega
nth_rw 1 [← partialTraj_comp_partialTraj h k.le_succ, hk, partialTraj_succ_self, comp_map, comap_map_comm,
comap_prod, id_comap, ← id_map, map_prod_eq, ← map_comp_right, this, map_comp_right, id_prod_eq, prodAssoc_prod,
map_comp_right, ← map_prod_map, map_id, ← map_comp, map_apply_eq_iff_map_symm_apply_eq, fst_prod_comp_id_prod, ←
map_comp_right, ← coe_IicProdIoc (h.trans k.le_succ), symm_comp_self, map_id,
deterministic_congr IicProdIoc_comp_restrict₂.symm, ← deterministic_comp_deterministic,
comp_deterministic_eq_comap, ← comap_prod, ← map_comp, ← comp_map, ← hk, ←
partialTraj_comp_partialTraj h k.le_succ, partialTraj_succ_self, map_comp, map_comp, ← map_comp_right, ← id_map,
map_prod_eq, ← map_comp_right]
· rfl
all_goals fun_prop
