Continuity of finite-time integrals of coordinate-product terms

This file proves continuity, under coordinatewise convergence of ordered times, of the finite-time-kernel integral of one PiContinuousMap.CoordinateProductTerm. The proof reduces to the coordinates on which the term has factors and applies the backward C₀ recursion.

When there are no active coordinates, the integrand is its scalar coefficient. That branch uses conservativity to identify the finite-time law as a probability measure; in particular, it never attempts to construct a constant-one element of C₀. This is finite-dimensional analytic infrastructure; no statement about path space is proved here.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.tendsto_integral_coordinateProductTerm_finiteTimeKernel {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {P : SubMarkovKernelSemigroup alpha} (hFeller : P.IsFellerKernelSemigroup) (hP : P.IsConservative) {X : Type u_2} {l : Filter X} {n : ℕ} {times : X → FiniteOrderedTimes n} {times0 : FiniteOrderedTimes n} (ht : ∀ (i : Fin n), Filter.Tendsto (fun (a : X) => (times a) i) l (nhds (times0 i))) (term : PiContinuousMap.CoordinateProductTerm (Fin n) alpha) (x : alpha) : Filter.Tendsto (fun (a : X) => ∫ (path : Fin n → alpha), term.toContinuousMap path ∂(P.finiteTimeKernel (times a)) x) l (nhds (∫ (path : Fin n → alpha), term.toContinuousMap path ∂(P.finiteTimeKernel times0) x))

The finite-time integral of a coordinate-product term varies continuously when every ordered time coordinate varies continuously.