partialTraj_map_frestrictLe₂_apply

English

For all a,b with Markov kernels κ, applying the map frestrictLe₂ to partialTraj a (b+1) yields partialTraj a b. This captures the idea that restricting the last coordinate does not affect the earlier segment.

Русский

Для всех a,b с марковскими ядрами κ применение отображения frestrictLe₂ к partialTraj a (b+1) дает partialTraj a b. Это выражает идею, что ограничение последней координаты не влияет на предыдущую часть траектории.

LaTeX

$$$ (partialTraj\,κ\,a\,(b+1)).map(frestrictLe₂\, b.le\,_{succ}) = partialTraj\,κ\,a\,b $$$

Lean4

theorem partialTraj_map_frestrictLe₂_apply (x₀ : Π i : Iic a, X i) (hbc : b ≤ c) :
    (partialTraj κ a c x₀).map (frestrictLe₂ hbc) = partialTraj κ a b x₀ := by
  rw [← map_apply _ (by fun_prop), partialTraj_map_frestrictLe₂]

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