Translation of finite dense-time kernels

This file transports the finite-set kernel translation law from physical nonnegative-real times to finite sets of dense times, using the canonical coordinate reindexings.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsConservative.finiteSetKernel_map_pullback_addFinset {alpha : Type u_1} [MeasurableSpace alpha] (P : SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (s : DenseTime) (I : Finset DenseTime) : (P.finiteSetKernel (denseTimePhysicalSet (s.addFinset I))).map (DenseTimePath.pullbackAddFinset s I ∘ DenseTimePath.pullbackPhysicalSet (s.addFinset I)) = ((P.finiteSetKernel (denseTimePhysicalSet I)).map (DenseTimePath.pullbackPhysicalSet I)).comp (P.kernel (DenseTime.castOrderEmbedding s))

Translating a finite dense-time observation set is the same as first evolving for the corresponding physical duration, after both physical and dense coordinates are reindexed.