Polish structure of continuous-path space

For a complete separable metric state space, the compact-open topology on continuous paths is Polish: it is second countable, and it is induced by the compact-convergence uniformity, which is complete and countably generated because nonnegative time is locally compact and sigma-compact. With the Borel sigma-algebra the path space is therefore a standard Borel space.

This is ordinary topological infrastructure. It proves no probabilistic statement.

instance MarkovProcess.ContinuousPath.instPolishSpace {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [SecondCountableTopology alpha] : PolishSpace (ContinuousPath alpha)

Continuous-path space over a complete separable metric space is Polish.

theorem MarkovProcess.ContinuousPath.standardBorelSpace_borel {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [SecondCountableTopology alpha] : StandardBorelSpace (ContinuousPath alpha)

With the Borel sigma-algebra, continuous-path space is a standard Borel space.