Convergence of the finite-dimensional laws of Feller semigroups

The finite-time results of Feller/FiniteTimeConvergence.lean, reindexed by a finite set of times. For conservative Feller kernel semigroups whose C₀ semigroups converge strongly, the finite-set laws converge against every compactly supported continuous test, uniformly in the starting point; and, at a fixed starting point, against every bounded continuous test, which is weak convergence of the finite-dimensional distributions.

The second statement cannot be uniform in the starting point: it uses the tightness of the limiting law at that point (Kernel/WeakConvergence.lean), and on a noncompact state space the finite-dimensional laws of a family of starting points escaping to infinity are not tight.

Main results: tendstoUniformly_integral_compactlySupported_finiteSetKernel, tendsto_integral_boundedContinuous_finiteSetKernel.

The set of observation times is fixed; nothing is asserted about joint convergence in the times and the semigroups.

theorem MarkovProcess.SubMarkovKernelSemigroup.tendstoUniformly_integral_compactlySupported_finiteSetKernel {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [LocallyCompactSpace alpha] [T2Space alpha] [SecondCountableTopology alpha] {iota : Type u_2} {l : Filter iota} {P : iota → SubMarkovKernelSemigroup alpha} {Q : SubMarkovKernelSemigroup alpha} (hP : ∀ (i : iota), (P i).IsFellerKernelSemigroup) (hPc : ∀ (i : iota), (P i).IsConservative) (hQ : Q.IsFellerKernelSemigroup) (hQc : Q.IsConservative) (hconv : ∀ (t : NNReal) (f : ZeroAtInftyContinuousMap alpha ℝ), Filter.Tendsto (fun (i : iota) => (⋯.c0Semigroup.operator t) f) l (nhds ((hQ.c0Semigroup.operator t) f))) (I : Finset NNReal) (f : CompactlySupportedContinuousMap (↥I → alpha) ℝ) : TendstoUniformly (fun (i : iota) (x : alpha) => ∫ (path : ↥I → alpha), f path ∂((P i).finiteSetKernel I) x) (fun (x : alpha) => ∫ (path : ↥I → alpha), f path ∂(Q.finiteSetKernel I) x) l

Uniform convergence of the finite-set laws against compactly supported tests.

theorem MarkovProcess.SubMarkovKernelSemigroup.tendsto_integral_boundedContinuous_finiteSetKernel {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [LocallyCompactSpace alpha] {iota : Type u_2} {l : Filter iota} {P : iota → SubMarkovKernelSemigroup alpha} {Q : SubMarkovKernelSemigroup alpha} (hP : ∀ (i : iota), (P i).IsFellerKernelSemigroup) (hPc : ∀ (i : iota), (P i).IsConservative) (hQ : Q.IsFellerKernelSemigroup) (hQc : Q.IsConservative) (hconv : ∀ (t : NNReal) (f : ZeroAtInftyContinuousMap alpha ℝ), Filter.Tendsto (fun (i : iota) => (⋯.c0Semigroup.operator t) f) l (nhds ((hQ.c0Semigroup.operator t) f))) (I : Finset NNReal) (f : BoundedContinuousFunction (↥I → alpha) ℝ) (x : alpha) : Filter.Tendsto (fun (i : iota) => ∫ (path : ↥I → alpha), f path ∂((P i).finiteSetKernel I) x) l (nhds (∫ (path : ↥I → alpha), f path ∂(Q.finiteSetKernel I) x))

Weak convergence of the finite-dimensional laws. At every starting point, the finite-set law of P i converges to that of Q against every bounded continuous test function.