English
If every κ_n is a zero-or-Markov kernel, then for all a, b the partial trajectory κ a b is still zero-or-Markov.
Русский
Если каждое κ_n является ноль-или-маркковским ядром, то частичная траектория κ a b остаётся ноль-или-маркковским ядром.
LaTeX
$$$ \forall a,b \in \mathbb{N},\ IsZeroOrMarkovKernel(\partialTraj\kappa a b) $$$
Lean4
instance [∀ n, IsZeroOrMarkovKernel (κ n)] (a b : ℕ) : IsZeroOrMarkovKernel (partialTraj κ a b) :=
by
obtain hab | hba := le_total a b
·
induction b, hab using Nat.le_induction with
| base => rw [partialTraj_self]; infer_instance
| succ k hak => rw [partialTraj_succ_of_le hak]; infer_instance
· rw [partialTraj_le hba]; infer_instance
