partialTraj_succ_eq_comp — Mathlib

English

For a ≤ b, the distribution from a to b+1 factors as the composition of the distribution from a to b with the distribution from b to b+1. Intuitively, the trajectory is built step by step and the joint law factors accordingly.

Русский

Пусть a ≤ b. Распределение траектории от a до b+1 факторизуется как композиция распределения от a до b и распределения от b до b+1. Интуитивно траектория строится шаг за шагом, и совокупное распределение расщепляется.

LaTeX

$$$ \partialTraj\,κ\,a\,b+1 = (\partialTraj\,κ\,b\,b+1) \circ_κ (\partialTraj\,κ\,a\,b) $$$

Lean4

theorem partialTraj_succ_eq_comp (hab : a ≤ b) :
    partialTraj κ a (b + 1) = partialTraj κ b (b + 1) ∘ₖ partialTraj κ a b := by
  rw [partialTraj_succ_self, ← map_comp, partialTraj_succ_of_le hab]

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