Referee responses and bibliography additions - #478
Conversation
- Add referee answer file (Report 69) with our responses - Bibliography: add Revuz–Yor, Ledoux–Talagrand, Marion (Ionescu–Tulcea), Douglas et al. (QFT) - Add "An alternative route" subsection (Lévy's construction) and a contributor list; assorted corrections and inline reviewer notes Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
| 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.) |
There was a problem hiding this comment.
This is another phrasing regarding the generality of the definition of Gaussian measures. The definition is actually general since it only requires to be a module with some topology, we just only proved interesting results for the Banach case. Bochner-Minlos I think is interesting regarding the existence of such measures but is not necessary to prove results about those measures. I also specify that although it has been auto-formalized this is somewhat different from what we have done since our goal is to get to mathlib which is significantly more difficult than just getting the formalization.
| \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?} |
There was a problem hiding this comment.
Probably we could but the existence theorem is for a general space where there is not necessarily a 0 so it would be weird to make this a special case in the construction.
…into pfaffelh_referee-revisions
3 participants
Revisions to the paper following the referee reports.
Changes
BM_paper/Answers_Report_69.texwith our responses to the reports.biblio.bib): added Revuz–Yor, Ledoux–Talagrand, Marion (Ionescu–Tulcea, arXiv:2506.18616), Douglas et al. (QFT, arXiv:2603.15770).main.tex:(X_t,X_t) → (X_s,X_t),Y_0 → Y_t).🤖 Generated with Claude Code