English
If every κ_n is a Markov kernel, then the partial trajectory κ a b is Markov for all a, b.
Русский
Если каждое κ_n является марковским ядром, то частичная траектория κ a b является марковским ядром для всех a, b.
LaTeX
$$$ \forall a,b \in \mathbb{N},\ IsMarkovKernel(\partialTraj\kappa a b) $$$
Lean4
instance [∀ n, IsMarkovKernel (κ n)] (a b : ℕ) : IsMarkovKernel (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]
have := IsMarkovKernel.map (κ k) (piSingleton k).measurable
exact IsMarkovKernel.map _ measurable_IicProdIoc
· rw [partialTraj_le hba]; infer_instance
