diff --git a/BM_paper/Answers_Report_69.tex b/BM_paper/Answers_Report_69.tex new file mode 100644 index 00000000..9dfe58b8 --- /dev/null +++ b/BM_paper/Answers_Report_69.tex @@ -0,0 +1,75 @@ +\documentclass[11pt]{article} + +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{amsmath,amssymb, xcolor} +\usepackage[margin=1in]{geometry} +\usepackage{hyperref} + +\newcommand{\TODO}[1]{\textcolor{teal}{TODO #1}} + +\begin{document} +\section*{Answers to the reports} +We thank both referees for their careful reading of the manuscript. Below are our answers. + +\paragraph{Report 6a...:} +The typos and small changed you suggest we carried out without further mentioning them. Here are the changes of more than one or two words: +\begin{itemize} + \item We have added a list of contributors to the repository with more than five commits. + \item Lemma 4.3 and footnote: done + \item Thm 4.7: You are right, $\sigma$-finiteness is not needed here. + \item Before Thm 4.20: xxx + \item In Thm 4.20, dependence $L(T,...)$ + \item Section 4.4.3: + \item Proposition 5.3: +\end{itemize} + +\paragraph{Report 69...:} + +\begin{itemize} + \item The author should mention the book by Revuz and Yor which is the most + definitive reference on the Brownian motion. + \\{\color{blue} We have added this book right at the beginning of the text.} + \item The definition of a stochastic process should appear clearly as a + definition (and maybe indicate which Lean predicate it refers to as for other + definitions?). + \\{\color{blue} \TODO{We should discuss this, I think. As far as I can see, defining what a stochastic process is does not really fit into Mathlib. Rather, it only involves some measurability assumptions, which we currently do not state explicitely.}} + \item The Kolmogorov continuity theorem for processes indexed by an abstract + spaces is classical and largely predates the work Kr\"atschmer and Urusov + [KU23] quoted in the paper (see for instance chapters 11 and 12 in the book + Ledoux and Talagrand, or Theorems 1.4.2 and 2.15.3 in the second edition + of Talagrand's book \emph{Upper and Lower Bounds for Stochastic Processes}). + In particular, when $(X_t)_{t \in T}$ is Gaussian, one can always equip $T$ with the + ``canonical'' pseudo-distance + \[ + d(s,t) := \mathbb{E}[(X_t - X_s)^2]^{1/2}, + \] + and deduce regularity from there. It is not clear to me what the advantage + of [KU23] is compared to the historical chaining approach and the authors + should at least quote a more standard reference in addition to [KU23]. + \\{\color{blue} Thanks for pointing us to these references, which we carefully checked. Our goal was to have a directly usable result which is most general. (For the latter reason, we do not want to restrict to the Gaussian case, covered in Chapter 12 and the book by Talagrand.) Although Ledoux and Talagrand formally restrict to the case of real-valued processes, we agree that their result is in fact more general that [KU23] since they use a Young function $\psi$, which must be specialized to $\psi(x) = x^p$ in [KU23]. However, Holder continuity in [KU23] is direct, and would have to be extracted from $\psi$ in LT, which is not immediate. We added a reference to [LT91] in 2.3.} + \item The authors define Gaussian random variables on Banach spaces but at the + most general level they can be defined on locally convex vector spaces. In + that regard, the Bochner--Minlos theorem guarantees existence of Gaussian + random variables on nuclear spaces (which incidentally can be used to + construct Gaussian fields). + \\{\color{blue}Thanks for pointing this out! Since the Bochner-Minlos theorem is not yet part of mathlib, this is not an option at the moment. We have added two sentences on the construction of Gaussian distributions on more general spaces at the end of 4.3.} + \item The simplest construction of the Brownian motion, and Gaussian field + in general, does not require Kolmogorov extension theorem. Consider a + Hilbert basis $(e_n)$ of $L^2(\mathbb{R}_+)$ and family $(G_n)$ of independent standard + Gaussian variables. For $f \in L^2$, set + \[ + X(f) := \sum_{n \in \mathbb{N}} \Bigl( \int_{\mathbb{R}_+} f(x) e_n(x)\,dx \Bigr) G_n, + \] + which converges in $L^2(\Omega)$. Then $B_t := X(\mathbf{1}_{[0,t]})$ is a Brownian motion. + Other Gaussian fields can be defined by changing the base Hilbert space. + \\{\color{blue}This basically leads to Lévy's construction of BM, where continuity of the sample paths is a rather direct result (if the proper base is chosen). We discussed this approach, but found that the path via Kolmogorov-Chentsov will pay off since it will be used more often (for processes rather than fields). We now refer to this construction in the new Section 2.5.} + \item The construction of the authors is correct and Kolmogorov extension + theorem is unavoidable for the construction of other stochastic processes + (for instance Markov processes). However, from a formalization point of + view it could be interesting to have the construction that relies on as few + results as possible on other results. + \\{\color{blue} Since Lean uses proof irrelevance, this statement can be debated. For example, real numbers in mathlib are based on Cauchy sequences rather than Dedekind cuts.} +\end{itemize} + +\end{document} diff --git a/BM_paper/biblio.bib b/BM_paper/biblio.bib index 2446041d..9690ff54 100644 --- a/BM_paper/biblio.bib +++ b/BM_paper/biblio.bib @@ -95,6 +95,18 @@ @book{karatzas1991brownian publisher = {Springer Science \& Business Media} } +@book{revuz1999continuous, + title = {Continuous martingales and Brownian motion}, + author = {Revuz, Daniel and Yor, Marc}, + series = {Grundlehren der mathematischen Wissenschaften}, + volume = {293}, + edition = {3}, + year = {1999}, + publisher = {Springer-Verlag, Berlin}, + isbn = {3-540-64325-7}, + doi = {10.1007/978-3-662-06400-9} +} + @book{morters2010brownian, title = {Brownian motion}, author = {M{\"o}rters, Peter and Peres, Yuval}, @@ -341,6 +353,33 @@ @Book{ talagrand2014 url = {https://doi.org/10.1007/978-3-642-54075-2} } +@article{marion2025ionescu, + title = {A Formalization of the {I}onescu-{T}ulcea Theorem in Mathlib}, + author = {Marion, Etienne}, + journal = {arXiv preprint arXiv:2506.18616}, + year = {2025} +} + +@article{douglas2026qft, + title = {Formalization of {QFT}}, + author = {Douglas, Michael R. and Hoback, Sarah and Mei, Anna and Nissim, Ron}, + journal = {arXiv preprint arXiv:2603.15770}, + year = {2026} +} + +@book{ledoux1991probability, + author = {Ledoux, Michel and Talagrand, Michel}, + title = {Probability in {B}anach Spaces. Isoperimetry and Processes}, + series = {Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results + in Mathematics and Related Areas (3)]}, + volume = {23}, + publisher = {Springer-Verlag, Berlin}, + year = {1991}, + pages = {xii+480}, + isbn = {3-540-52013-9}, + doi = {10.1007/978-3-642-20212-4} +} + @book{LeGall2016, author = {Le Gall, Jean-Fran{\c{c}}ois}, title = {Brownian motion, martingales, and stochastic calculus}, diff --git a/BM_paper/main.tex b/BM_paper/main.tex index 40ee37c8..2c315b85 100644 --- a/BM_paper/main.tex +++ b/BM_paper/main.tex @@ -95,7 +95,7 @@ \section{Introduction} \subsection{Mathematical background} -\sloppy Brownian motion is arguably one of the most important stochastic processes (e.g.\ \cite{karatzas1991brownian, morters2010brownian}), and is used as a modeling tool across all sciences (physics: e.g.\ \cite{einstein1906theorie, bian2016111}; biology: e.g.\ \cite{erban2014molecular}; finance: e.g.\ \cite{davis2006louis}). Mathematically, Brownian motion led to the Wiener measure \cite{wiener1923differential}, which is the first instance of a probability measure on a function space, but also to developments such as Stochastic (Partial) Differential equations (see e.g.\ \cite{hairer2009introduction}). +\sloppy Brownian motion is arguably one of the most important stochastic processes (e.g.\ \cite{karatzas1991brownian, revuz1999continuous, morters2010brownian}), and is used as a modeling tool across all sciences (physics: e.g.\ \cite{einstein1906theorie, bian2016111}; biology: e.g.\ \cite{erban2014molecular}; finance: e.g.\ \cite{davis2006louis}). Mathematically, Brownian motion led to the Wiener measure \cite{wiener1923differential}, which is the first instance of a probability measure on a function space, but also to developments such as Stochastic (Partial) Differential equations (see e.g.\ \cite{hairer2009introduction}). The goal of the present paper is to describe a formalization of Brownian motion using \Lean \cite{lean, moura2021lean}, building on its mathematical library \mathlib \cite{mathlib}. For this paper we use the following definition of Brownian motion (there are many equivalent characterizations, e.g.\ Definition 2.12 with Proposition 2.3 of~\cite{LeGall2016}). @@ -157,7 +157,7 @@ \subsection{Project organization} We started by implementing in \Lean several key definitions and statements (without proofs): there are always several ways to turn a mathematical concept into a \Lean definition, and in order to collaborate on a project it is important to decide early on a unique way to talk about any concept to ensure compatibility of the code produced, even if the definition chosen can then be refined. Different parts of the blueprint had different levels of details: we wrote a precise description of the technical Kolmogorov-Chentsov proof, but omitted many proofs for more standard results on Gaussian distributions. -The project was announced on the \href{https://leanprover.zulipchat.com/}{Lean Zulip website}, and anyone interested was invited to contribute. D.L. and E.M. joined the project at that time and then contributed significantly to the formalization. The coordination of the project was done through discussions in a Zulip channel: lists of tasks and progress updates were regularly posted, and volunteers could claim the tasks and report on their progress. +The project was announced on the \href{https://leanprover.zulipchat.com/}{Lean Zulip website}, and anyone interested was invited to contribute. D.L. and E.M. joined the project at that time and then contributed significantly to the formalization. The coordination of the project was done through discussions in a Zulip channel: lists of tasks and progress updates were regularly posted, and volunteers could claim the tasks and report on their progress. (The full list of contributors -- excluding authors of the present manuscript -- with more than five commits is: Eugenio Cainelli, Markus Himmel, Nikolas Kuhn, Yongxi (Aaron) Lin, Lorenzo Luccioli, Jack McCarthy, Pietro Monticone, Jérémy Scanvic, Kexing Ying, Thomas Zhu.) The correctness of the code was ensured by continuous integration scripts on github, which automatically check that the code compiles without errors, and by manual review of the proposed additions. The blueprint continued to evolve during the formalization, as new lemmas were added (once because a small gap was identified in the blueprint proof), definitions were changed to better fit the needs of writing in \Lean, and small mistakes were corrected (particularly in the exact value of constants used in the Kolmogorov-Chentsov proof). @@ -233,7 +233,7 @@ \subsection{The Kolmogorov-Chentsov Theorem} Therefore, $X_t = Y_t$ almost surely. We will use a more general version of this statement, replacing $T = [0,1]$ by a metric space with a property restricting the number of balls needed to cover $T$. The version we formalize is based on -the recent work of~\cite{kratschmer2023kolmogorov}. +the recent work of~\cite{kratschmer2023kolmogorov}. (Note the similar approach taken by \cite[Chapter~11]{ledoux1991probability}, which is based on real-valued processes, and which gives less concrete bounds, especially for Holder continuity.) \subsection{Construction of Brownian motion and Wiener measure on $\R_+$} @@ -246,8 +246,8 @@ \subsection{Construction of Brownian motion and Wiener measure on $\R_+$} So, we obtain from that theorem a process with continuous paths and the correct finite dimensional distributions, which we call Brownian motion. This also gives a distribution on the continuous functions $\mathcal C(\mathbb R_+, \mathbb R)$, which is the Wiener measure. - - +\subsection{An alternative route} +Our way to construct Brownian Motion is not the only one possible. In particular, Lévy's construction of Brownian Motion gives a more direct construction. Here, one takes an infinite number of independent $N(0,1)$-distributed random variables (e.g.\ obtained via the Ionescu-Tulcea Theorem, formalized in \cite{marion2025ionescu}), constructs Brownian Motion on all dyadic numbers, and obtains a stochastic process with continuous paths by extension to $\mathbb R_{\geq 0}$. See e.g.\ Chapter 1.1.3 in \cite{morters2010brownian}. Since we aim for an approach which is useful also for constructing other stochastic processes, we do not follow this path. \section{Random variable formalism} \label{S:RV-formalism} @@ -433,7 +433,7 @@ \subsubsection{Carathéodory's Extension Theorem} \begin{theorem}[Carathéodory extension]\label{T:masseind} Let $\mathcal H$ be a semi-ring and $m: \mathcal H\to\mathbb R_+$ - $\sigma$-finite and $\sigma$-additive. Furthermore, let $\mu$ be the + $\sigma$-additive. Furthermore, let $\mu$ be the induced outer measure from Proposition~\ref{P:auss} and $\mathcal F$ the $\sigma$-algebra from Theorem~\ref{T:cara}. Then, $\sigma(\mathcal H)\subseteq\mathcal F$ and $\mu$ coincides with $m$ @@ -553,9 +553,13 @@ \subsection{Gaussian Measures and characteristic functions} Prior to our work, \mathlib contained the definition of the one-dimensional normal distribution \mllink{Probability/Distributions/Gaussian/Real}{L198-L201}{ProbabilityTheory.gaussianReal}, but not more general Gaussian measures. We will denote by $N(m, \sigma^2)$ the normal distribution on $\mathbb{R}$ with mean $m$ and variance $\sigma^2$. In order to define the law of a Brownian motion on $\mathbb{R}_+$, we need definitions and properties of multivariate Gaussian distributions. -We did not however define Gaussian measures only for that setting, but first introduced a general definition for Banach spaces, and then specialized it to Hilbert and finally finite dimensional spaces. +We did not however define Gaussian measures only for that setting, but first introduced a general definition which makes sense in an arbitrary module equipped with a topology. Then we proved several results for general Banach spaces, and specialized some of them to Hilbert spaces and finally finite dimensional spaces. Our formalization uses many results from \mathlib and we relied on characteristic functions \mllink{MeasureTheory/Measure/CharacteristicFunction}{L322-L325}{MeasureTheory.charFunDual}, as well as the fact that they uniquely determine a probability measure \mllink{MeasureTheory/Measure/CharacteristicFunction}{L435-L439}{MeasureTheory.Measure.ext_of_charFunDual}. +Note that some results could be generalized on more general spaces, namely locally convex vector spaces. One could in particular aim for a formalization of the Bochner-Minlos Theorem, which is not yet available in \mathlib. (Note that this result was recently auto-formalized for the development of Quantum Field Theory in \cite{douglas2026qft}, although it would require a lot of work to upstream it to \mathlib.) + +Note that Gaussian distributions could be defined on more general spaces (locally convex vector spaces). The construction requires a formalization of the Bochner-Minlos Theorem, which is not yet available in \mathlib. (However, note that this result was recently formalized for the development of Quantum Field Theory in \cite{douglas2026qft}.) + \subsubsection{Gaussian distributions} @@ -676,14 +680,14 @@ \subsubsection{The Kolmogorov condition} \begin{definition}[Kolmogorov condition]\label{def:kolmogorov_condition} Let $p, q, M$ be non-negative real numbers with $p,q>0$. -A stochastic process $(X_t)_{t \in T}$ is said to satisfy the Kolmogorov condition for exponents $(p, q)$ with constant $M$ if for all $s, t \in T$, the pair $(X_t, X_t) : \Omega \to E \times E$ is measurable for the Borel $\sigma$-algebra on $E \times E$, and +A stochastic process $(X_t)_{t \in T}$ is said to satisfy the Kolmogorov condition for exponents $(p, q)$ with constant $M$ if for all $s, t \in T$, the pair $(X_s, X_t) : \Omega \to E \times E$ is measurable for the Borel $\sigma$-algebra on $E \times E$, and \begin{align*} \mathbf{E}[d_E(X_s, X_t)^p] \le M d_T(s, t)^q \: . \end{align*} \end{definition} -The measurability condition ensures that the distance $d_E(X_s, X_t)$ is a measurable. +The measurability condition ensures that the distance $d_E(X_s, X_t)$ is measurable. If $E$ was second-countable, we could simply assume that $X_s$ is measurable for all $s \in T$, and the measurability of the pair would follow. This is because for a second-countable space $E$, $\mathcal{B}(E \times E)$ is the product of the Borel $\sigma$-algebras on $E$, which is not true in general. @@ -696,6 +700,8 @@ \subsubsection{The main theorem} We formalize a recent and general version of the Kolmogorov-Chentsov theorem \cite[Theorem 1]{kratschmer2023kolmogorov}, which applies to extended pseudo-metric spaces under a covering assumption on the index set $T$. We say that $T$ has bounded covering number with constant $c > 0$ and exponent $d \ge 0$ if for all $\varepsilon \in (0, \mathrm{diam}(T)]$, $T$ can be covered by at most $c \varepsilon^{-d}$ balls of radius $\varepsilon$ (see Definition~\ref{def:bounded_covering_number} below). Note that such a space is totally bounded by construction. +{\color{blue} xxx Maybe add "Note also that this condition implies $diam(T) < \infty$, even if $T$ is an extended metric space to start with".} + \begin{theorem}[Kolmogorov-Chentsov]\label{thm:kolmogorov_chentsov} Suppose that the index set $T$ has bounded covering number with constant $c>0$ and exponent $d > 0$. Let $(X_t)_{t \in T}$ be a stochastic process that satisfies the Kolmogorov condition for exponents $(p,q)$ with constant $M$, with $q > d$ and $p > 0$. @@ -705,6 +711,7 @@ \subsubsection{The main theorem} \le M L(T, c, d, p, q, \beta) \: . \end{align*} +{\color{blue}xxx If L is supposed to be a universal constant, I don't see how it could depend on $T$. Does it really? (Note that if it only depends on $T$ through its diameter, then in fact it doesn't depend on $T$ since the diameter can be bounded in terms of $c$ and $d$: for epsilon with $c \epsilon^{-d} < 1$, the covering condition would say that $T$ is bounded by $0$ balls, which is a contradiction; so this epsilon is $> diam T$, which gives you the claimed bound on the diameter)} If furthermore $E$ is complete and $T$ is second-countable, then the process $X$ has a modification with Hölder continuous paths of exponent $\beta$ for all $\beta \in (0, (q - d)/p)$. \end{theorem} @@ -751,7 +758,7 @@ \subsubsection{The main theorem} \end{theorem} The hypothesis on $T$ is satisfied for $T = \mathbb{R}_+$, with $T_n = [0,n)$ (which is open in $\mathbb{R}_+$), for $d = 1$. -Although we use it only for $T = \mathbb{R}_+$, Theorem~\ref{thm:localized_holder_modification_sup} can be used in higher dimension and in more involved cases: the authors of \cite{kratschmer2023kolmogorov} show how to apply it to subsets of $m$-dimensional Riemannian manifolds. +Although we use it only for $T = \mathbb{R}_+$, Theorem~\ref{thm:localized_holder_modification_sup} can be used in higher dimension and in more involved cases: the authors of \cite{kratschmer2023kolmogorov} show how to apply it to subsets of $d$-dimensional Riemannian manifolds. We don't describe the proof of Theorem~\ref{thm:localized_holder_modification_sup} in detail here (we refer the reader to \cite{kratschmer2023kolmogorov}, or to the code): it consists in applying the same type of arguments as in the proof of the second part of Theorem~\ref{thm:kolmogorov_chentsov} to build separately modifications for each set $T_n$ and exponents ($p_m, q_m)$ and then combine them into one process (see section~\ref{sub:holder_process}). @@ -767,7 +774,7 @@ \subsubsection{Covers and chaining} \paragraph{Covers} An (internal) $\varepsilon$-cover of $T$ is a subset $S \subseteq T$ such that for all $t \in T$, there exists $s \in S$ such that $d_T(s, t) \le \varepsilon$. -If $T$ has bounded diameter we can find an $\varepsilon$-cover which is finite, and the covering number of $T$ for $\varepsilon > 0$ is the minimal cardinality of an $\varepsilon$-cover of $T$, denoted by $N_\varepsilon(T)$. +If $T$ has bounded diameter we can find an $\varepsilon$-cover which is finite {\color{blue} xxx Not true in general (the unit ball in an infinite-dimensional Hilbert space is a counterexample). You need total boundedness here.}, and the covering number of $T$ for $\varepsilon > 0$ is the minimal cardinality of an $\varepsilon$-cover of $T$, denoted by $N_\varepsilon(T)$. We call a cover with that cardinality a minimal $\varepsilon$-cover. Our formalization also includes definitions of external covers and covering numbers, packing numbers and inequalities between these numbers and the volume of balls. We don't detail those here, but the relations between those quantities are helpful to prove properties of covering numbers. @@ -833,7 +840,7 @@ \subsubsection{Covers and chaining} \subsubsection{Proof of the main inequality} -Under the assumptions of Theorem~\ref{thm:kolmogorov_chentsov}, we prove that for all countable subset $T' \subseteq T$, +Under the assumptions of Theorem~\ref{thm:kolmogorov_chentsov}, we prove that for any countable subset $T' \subseteq T$, \begin{align*} \mathbf{E}\left[ \sup_{s, t \in T'} \frac{d_E(X_s, X_t)^p}{d_T(s, t)^{\beta p}} \right] \le M L(T, c, d, p, q, \beta) @@ -916,7 +923,7 @@ \subsubsection{Proof of the main inequality} \end{align*} Since $\varepsilon_m \le \delta \le 4 \varepsilon_m$, we obtain a bound of order $\delta^{q - 2d}$, which is not sufficient to conclude the proof with the right exponent $\delta^{q - d}$. The issue is the square on the cardinal of the cover $C_m$, and this is where the pair reduction lemma (Lemma~\ref{lem:pair_reduction}) comes into play. -With that lemma applied to $a = 2$, $n = \lceil \log_2 J \rceil$ and $c = 8 \varepsilon_m$, we obtain a set $K \subseteq C_m^2$ with $\lvert K \rvert \le 2 \lvert C_m \rvert$ and $\sup_{(s, t) \in K} d_T(s, t) \le 8 n \varepsilon_m$, such that an application of \eqref{eq:kolmogorov_condition_finite_set} gives +With that lemma applied to $a = 2$, $n = \lceil \log_2 J \rceil$ {\color{blue}xxx Should $J$ it be $C_m$?} and $c = 8 \varepsilon_m$, we obtain a set $K \subseteq C_m^2$ with $\lvert K \rvert \le 2 \lvert C_m \rvert$ and $\sup_{(s, t) \in K} d_T(s, t) \le 8 n \varepsilon_m$, such that an application of \eqref{eq:kolmogorov_condition_finite_set} gives \begin{align*} \mathbf{E}\left[ \sup_{\substack{s, t \in C_m \\ d_T(s, t) \le 8 \varepsilon_m}} d_E(X_s, X_t)^p \right] &\le 2^p \mathbf{E}\left[ \sup_{s, t \in K} d_E(X_s, X_t)^p \right] @@ -937,7 +944,7 @@ \subsubsection{Proof of the main inequality} \le \sum_{i=m}^{N-1} \mathbf{E}\left[\sup_{s \in C_N} d_E(X_{\bar{s}_{i+1}}, X_{\bar{s}_i})^p\right] \: . \end{align*} -It remains to control the expectation inside the sum, which we do using the Kolmogorov condition though Equation~\eqref{eq:kolmogorov_condition_finite_set} with $K = \{(\bar{s}_{i+1}, \bar{s}_i) \mid s \in C_N\}$. That set has cardinal at most $\lvert C_{i+1} \rvert$ (the number of possible values for $\bar{s}_{i+1}$, since $\bar{s}_i$ is a function of $\bar{s}_{i+1}$). +It remains to control the expectation inside the sum, which we do using the Kolmogorov condition through Equation~\eqref{eq:kolmogorov_condition_finite_set} with $K = \{(\bar{s}_{i+1}, \bar{s}_i) \mid s \in C_N\}$. That set has cardinal at most $\lvert C_{i+1} \rvert$ (the number of possible values for $\bar{s}_{i+1}$, since $\bar{s}_i$ is a function of $\bar{s}_{i+1}$). \begin{align*} \mathbf{E}\left[\sup_{s \in C_N} d_E(X_{\bar{s}_{i+1}}, X_{\bar{s}_i})^p\right] &\le M \lvert C_{i+1} \rvert \varepsilon_i^q @@ -986,7 +993,7 @@ \subsubsection{Building a Hölder continuous process} It is actually only a ``distance zero modification'', by which we mean that $d_E(X_t, Y_t) = 0$ almost surely. Since $E$ is only a pseudo-metric space, $Y$ might not satisfy the modification property $Y_t = X_t$ almost surely. We refer to \cite{kratschmer2023kolmogorov} for the proof that $Y$ is a distance zero modification of $X$\footnote{They use a metric space assumption for $E$ and prove that $Y$ is a true modification: replacing equalities with distance zero statements gives our proof for pseudo-metric spaces.}, and only note that it uses convergence in probability, which we had to generalize in \mathlib from pseudo-metric to extended pseudo-metric spaces. -From a distance zero modification $Y$ of $X$, we can obtain a true modification in a pseudo-metric space as follows: for each $t \in T$, let $Z_t$ be equal to $X_t$ on the event where $d_E(X_t, Y_t) = 0$, and equal to $Y_0$ otherwise. +From a distance zero modification $Y$ of $X$, we can obtain a true modification in a pseudo-metric space as follows: for each $t \in T$, let $Z_t$ be equal to $X_t$ on the event where $d_E(X_t, Y_t) = 0$, and equal to $Y_t$ otherwise. Then $Z_t = X_t$ almost surely, and since $d_E(Z_t(\omega), Y_t(\omega)) = 0$ for all $t$ and all $\omega$, $Z$ has the same continuity properties as $Y$. Finally, $Z$ is measurable (that is, $Z_t$ is measurable for all $t$), since a random variable that is at distance zero from a measurable random variable is itself measurable. @@ -1021,7 +1028,7 @@ \section{Construction of a Brownian motion and Wiener measure} We build a stochastic process $(B_t)_{t \in \mathbb{R}_+}$ such that \begin{itemize} \item $B$ has continuous paths, - \item $B_0 = 0$ almost surely, + \item $B_0 = 0$ almost surely, {\color{blue} Can't you even guarantee that $B_0 = 0$ everywhere, by taking $x_0 = 0$ in the construction of $Y_t$ on Page 32?} \item for all $n \in \mathbb{N}$ and $t_1, \ldots, t_n \in \mathbb{R}_+$, the vector $(B_{t_1}, \ldots, B_{t_n})$ has a multivariate normal distribution with mean $0$ and covariance matrix given by $\mathbf{cov}(B_{t_i}, B_{t_j}) = t_i \wedge t_j$. \end{itemize} @@ -1031,10 +1038,11 @@ \section{Construction of a Brownian motion and Wiener measure} Let $(C_t)_{t \in \mathbb{R}_+}$ be the canonical process on $\mathbb{R}^{\mathbb{R}_+}$, defined by $C_t(\omega) = \omega(t)$ for all $\omega \in \mathbb{R}^{\mathbb{R}_+}$. The process $C$ is measurable, and its finite-dimensional distributions in the measure space $(\mathbb{R}^{\mathbb{R}_+}, P_B)$ are the projective family we defined. -Finally, we check that $C$ satisfies the Kolmogorov condition for exponents $(2n, n)$ for all $n \in \mathbb{N}$ with constant $M = (2n - 1)!!$ (the double factorial, product of all odd integers up to $2n - 1$). +Finally, we check that $C$ satisfies the Kolmogorov condition for exponents $(2n, n)$ for all $n \in \mathbb{N}$ with constant $M = (2n - 1)!!$ (the double factorial, product of all odd integers up to $2n - 1$). {\color{blue} Just to clarify, wouldn't the condition for $(2, 1)$ be enough to get Hölder continuous path with any exponent $<1/2$?} We can then apply Theorem~\ref{thm:localized_holder_modification_sup} to obtain a modification $B$ of $C$ with locally Hölder continuous paths of all orders $\gamma \in (0, 1/2)$. In particular, $B$ has continuous paths. The process $B$ is a Brownian motion indexed by $\mathbb{R}_+$ with values in $\mathbb{R}$. +Note that it is important to have the Kolmogorov condition for all exponents $(2n, n)$ to obtain Hölder continuity for $\gamma < 1/2$, as in this case Theorem~\ref{thm:localized_holder_modification_sup} gives Hölder continuity for $\gamma < \sup_n \frac{n-1}{2n} = 1/2$. \paragraph{Properties of the Brownian motion} @@ -1093,7 +1101,7 @@ \section{Construction of a Brownian motion and Wiener measure} In particular, the way to prove Proposition~\ref{prop:isBrownianOfIndep} is to first show that the hypotheses imply that the process is Gaussian, and then apply Proposition~\ref{prop:isBrownianOfCov}. To do that we prove this more general result: \begin{lemma}[\bmlink{Gaussian/BrownianMotion}{L161-L168}{ProbabilityTheory.HasIndepIncrements.isGaussianProcess}] -Let $E$ be a second-countable Banach space and $T$ be an index set that is linearly ordered with a least element $\bot$. Consider $(X_t)_{t \in T}$ an $E$-valued stochastic process with independent increments, and such that for all $t$, $X_t$ has a Gaussian law. Further assume that $X_\bot$ is almost surely equal to $0$. Then $X$ is a Gaussian process. +Let $E$ be a second-countable Banach space and $T$ be a linearly ordered index set with a least element $\bot$. Consider $(X_t)_{t \in T}$ an $E$-valued stochastic process with independent increments, and such that for all $t$, $X_t$ has a Gaussian law. Further assume that $X_\bot$ is almost surely equal to $0$. Then $X$ is a Gaussian process. \end{lemma} This is probably the lemma which required most work. The idea is to say that $(X_{t_1}, ..., X_{t_n})$ can be expressed as a linear combination of the increments $(X_{t_1} - X_\bot, ..., X_{t_n} - X_{t_{n-1}})$. Because the increments are independent and each $X_t$ is Gaussian, we can prove that each increment is Gaussian. Because they are independent, their linear combination is also Gaussian, and so $(X_{t_1}, ..., X_{t_n})$ is Gaussian. Making the linear combination explicit and proving the equality was rather technical.