partialTraj_comp_partialTraj' — Mathlib

English

Under Markov kernel assumptions, composing the partial trajectories from a to b and from b to c yields the partial trajectory from a to c. This extends the chain rule to kernels.

Русский

При условии марковских ядер композиция частичных траекторий от a к b и от b к c дает частичную траекторию от a к c. Это расширяет правило цепи к ядерным распределениям.

LaTeX

$$$ (partialTraj\,κ\,b\,c).comp (partialTraj\,κ\,a\,b) = partialTraj\,κ\,a\,c $$$

Lean4

/-- Same as `partialTraj_comp_partialTraj` but only assuming `a ≤ b`. It requires Markov kernels. -/
theorem partialTraj_comp_partialTraj' (c : ℕ) (hab : a ≤ b) :
    partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c :=
  by
  obtain hbc | hcb := le_total b c
  · rw [partialTraj_comp_partialTraj hab hbc]
  · rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]

Похожие утверждения