PseudoEMetricSpace in Kolmogorov-Chentsov

Stream: Brownian motion

[Rémy Degenne]

This is motivated by a discussion I had with @Peter Pfaffelhuber , who was surprised that we need EMetricSpace and not PseudoEMetricSpace for the space of values of the process to get the existence of a Hölder modification in the Kolmogorov-Chentsov theorem (for this theorem for example).

Why do we need the space to be metric, and not only pseudo-metric? Well, to obtain a modification $Y$ of a process $X$, such that for all $t$, $Y_t = X_t$ a.e., we say that it suffices to show $d_E(Y_t, X_t) = 0$ a.e. So this is the (first) reason, but then comes the question of what we can get in a pseudo-metric space. Can we get a "distance zero modification", such that $d_E(Y_t, X_t) = 0$ a.e., or are we using metric elsewhere?
It turns out that we are currently using metric elsewhere.

When we build a Hölder modification for one exponent $Y_t^\beta$, we also prove that it is a limit of $X$: we have $Y_t^\beta = \lim_{s \in T', s \to t} X_s$ (simplifying a bit). Same thing for $Y_t^\gamma$ for another exponent. We then want to build a modification that is Hölder for both exponents, and for measurability reasons, the construction we use needs the pairs $(X_s^\beta, Y_t^\gamma)$ to be measurable for all $(s, t)$ (remember that we don't have a second-countable space, so measurability of the pair does not follow from the individual measurability alone).
The way we currently do it is roughly as follows: we know that $(X_s, X_t)$ is measurable for all $(s,t)$. We write $(Y_s^\beta, Y_t^\gamma) = (\lim_{s' \in T', s' \to s} X_s', \lim_{t' \in T', t' \to t} X_t') = \lim_{s',t' \in T', (s',t') \to (s,t)} (X_s', X_t')$ and that last limit is measurable. But here is the issue: the last equality uses the fact that the space is metric and not just pseudo-metric.

In a pseudo-metric space, say that $y_s^{(1)}$ and $y_s^{(2)}$ are at distance 0. Then if $X_s'$ tends to $y_s^{(1)}$ as $s'$ tends to $s$ in $T'$, then it tends also to $y_s^{(2)}$. The way the limit is defined in Lean is that it picks an arbitrary element among the possible limits.
Then we can have $(\lim_{s' \in T', s' \to s} X_s', \lim_{t' \in T', t' \to t} X_t') = (y_s^{(1)}, y_t)$ but $\lim_{s',t' \in T', (s',t') \to (s,t)} (X_s', X_t') = (y_s^{(2)}, y_t)$ and the equality we used does not hold.

I'm curious about possible solutions to get to a distance zero modification that is Hölder for several exponents. I started trying to generalize in the draft PR https://github.com/RemyDegenne/brownian-motion/pull/300 and that's how I encountered the issue.

[Sébastien Gouëzel]

Naïve question: if d (X, Y) = 0 everywhere and X is measurable, is Y also measurable?

[Rémy Degenne]

That would replace the equality of limits with the distance zero statement, and then we would transfer measurability that way, I see. I don't know the answer to that question yet, though.

[Sébastien Gouëzel]

The question is whether {a | Y a \in U} is measurable when U is open. But if d (X, Y) = 0 everywhere, X a belongs to U iff Y a does, so this set is {a | X a \in U}, so it is indeed measurable. Right?

[Rémy Degenne]

Looks good. That's solved then. Thanks! :tada: I'll implement that.