English
This technical lemma states that partialTraj a b can be decomposed into two independent parts, with the first part being the identity. This separation is crucial for computing integrals in the trajectory construction.
Русский
Эта техническая лемма говорит, что partialTraj a b раскладывается на две независимые части, первая из которых является тождественным распределением. Это разделение важно для вычисления интегралов в конструировании траектории.
LaTeX
$$$ \partialTraj\,κ\,a\,b = (\mathrm{Id} \times\_k (\partialTraj\,κ\,a\,b).map(\mathrm{restrict}_2\ Ioc\_subset\_Iic\_self)).map(IicProdIoc\,a\,b)$$$
Lean4
theorem partialTraj_succ_map_frestrictLe₂ (a b : ℕ) :
(partialTraj κ a (b + 1)).map (frestrictLe₂ b.le_succ) = partialTraj κ a b :=
by
obtain hab | hba := le_or_gt a b
· have := IsMarkovKernel.map (κ b) (piSingleton b).measurable
rw [partialTraj_succ_eq_comp hab, map_comp, partialTraj_succ_self, ← map_comp_right, frestrictLe₂_comp_IicProdIoc, ←
fst_eq, fst_prod, id_comp]
all_goals fun_prop
· rw [partialTraj_le (Nat.succ_le.2 hba), partialTraj_le hba.le, deterministic_map]
· rfl
· fun_prop
