Continuity tools for finite-time Feller kernels

This file records the analytic continuity mechanism needed in a recursive proof of continuity of finite-time laws. In particular, strong continuity and contractivity imply joint continuity in the time and in a varying C₀ test function. After evaluation, this gives convergence of kernel integrals when both the transition time and the test function vary.

The extension from product tests to arbitrary compactly supported tests on a finite product is not asserted here.

theorem MarkovProcess.Semigroup.StronglyContinuousContractionSemigroup.tendsto_apply_of_tendsto {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : StronglyContinuousContractionSemigroup E) {X : Type u_2} {l : Filter X} {t : X → NNReal} {t₀ : NNReal} {f : X → E} {f₀ : E} (ht : Filter.Tendsto t l (nhds t₀)) (hf : Filter.Tendsto f l (nhds f₀)) : Filter.Tendsto (fun (x : X) => (S.operator (t x)) (f x)) l (nhds ((S.operator t₀) f₀))

A strongly continuous contraction semigroup acts continuously when both time and the vector vary. Strong continuity alone only states this for a fixed vector; contractivity makes the dependence on the vector uniform in time.

theorem MarkovProcess.Semigroup.StronglyContinuousContractionSemigroup.continuous_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : StronglyContinuousContractionSemigroup E) : Continuous fun (tf : NNReal × E) => (S.operator tf.1) tf.2

Joint continuity of the semigroup action in time and the evolving vector.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.tendsto_kernelIntegral_c0 {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsFellerKernelSemigroup) {X : Type u_2} {l : Filter X} {t : X → NNReal} {t₀ : NNReal} {f : X → ZeroAtInftyContinuousMap alpha ℝ} {f₀ : ZeroAtInftyContinuousMap alpha ℝ} (ht : Filter.Tendsto t l (nhds t₀)) (hf : Filter.Tendsto f l (nhds f₀)) (x : alpha) : Filter.Tendsto (fun (a : X) => kernelIntegral (P.kernel (t a)) (⇑(f a)) x) l (nhds (kernelIntegral (P.kernel t₀) (⇑f₀) x))

Feller continuity permits both the time and the C₀ integrand to vary.

theorem MarkovProcess.SubMarkovKernelSemigroup.IsFellerKernelSemigroup.tendsto_twoStepProduct_c0 {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {P : SubMarkovKernelSemigroup alpha} (hP : P.IsFellerKernelSemigroup) {X : Type u_2} {l : Filter X} {t s : X → NNReal} {t₀ s₀ : NNReal} {f g : X → ZeroAtInftyContinuousMap alpha ℝ} {f₀ g₀ : ZeroAtInftyContinuousMap alpha ℝ} (ht : Filter.Tendsto t l (nhds t₀)) (hs : Filter.Tendsto s l (nhds s₀)) (hf : Filter.Tendsto f l (nhds f₀)) (hg : Filter.Tendsto g l (nhds g₀)) (x : alpha) : Filter.Tendsto (fun (a : X) => kernelIntegral (P.kernel (t a)) (⇑(f a) * ⇑((hP.c0Semigroup.operator (s a)) (g a))) x) l (nhds (kernelIntegral (P.kernel t₀) (⇑f₀ * ⇑((hP.c0Semigroup.operator s₀) g₀)) x))

The two-transition backward recursion is continuous for product C₀ tests. The inner transition acts on g; multiplication by the first-coordinate test f gives the varying C₀ test seen by the outer transition. This is the successor-step analytic mechanism in the finite-time argument.