Kolmogorov support for dense-time trajectory kernels

This file applies the global dyadic-floor modification to the coordinate process of a dense-time trajectory kernel. A parameterwise Kolmogorov moment condition implies that the dense-time law is supported on restrictions of continuous paths.

No measurability of the totalized modification as a path-valued map, PDE increment estimate, Markov property of the resulting paths, or Hunt-process assertion is made here.

theorem MarkovProcess.Kernel.IsSupportedOnContinuousPaths.of_isKolmogorovCoordinate {beta : Type u_1} {alpha : Type u_2} [MeasurableSpace beta] [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] (kappa : ProbabilityTheory.Kernel beta (DenseTime → alpha)) [ProbabilityTheory.IsMarkovKernel kappa] (hK : ∀ (b : beta), ∃ (p : ℝ) (q : ℝ) (gamma : ℝ) (M : NNReal), ProbabilityTheory.IsKolmogorovProcess (fun (r : DenseTime) (omega : DenseTime → alpha) => omega r) (kappa b) p q M ∧ 0 < gamma ∧ gamma < (q - 1) / p) : IsSupportedOnContinuousPaths kappa

A parameterwise Kolmogorov moment estimate for the canonical coordinate process implies almost-sure support of every dense-time trajectory law on restrictions of continuous paths. The constants and exponents may depend on the kernel parameter.

theorem MarkovProcess.Kernel.map_denseRestriction_toContinuousPathKernel_of_isKolmogorovCoordinate {beta : Type u_1} {alpha : Type u_2} [MeasurableSpace beta] [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] (kappa : ProbabilityTheory.Kernel beta (DenseTime → alpha)) [ProbabilityTheory.IsMarkovKernel kappa] (default : ContinuousPath alpha) (hK : ∀ (b : beta), ∃ (p : ℝ) (q : ℝ) (gamma : ℝ) (M : NNReal), ProbabilityTheory.IsKolmogorovProcess (fun (r : DenseTime) (omega : DenseTime → alpha) => omega r) (kappa b) p q M ∧ 0 < gamma ∧ gamma < (q - 1) / p) : (toContinuousPathKernel kappa default).map ContinuousPath.denseRestriction = kappa

Under the coordinate Kolmogorov estimate, transporting to continuous paths and restricting back to dense time recovers the original trajectory kernel. The path-space transport uses only the already established measurable extension map.