The Wasserstein cost of the Girsanov Theorem
Simon Coste
math.PR
Nov 11, 2026 · v1
math.FA
TL;DR
Provides a Lean 4 formalization of the main Wasserstein asymptotics, built on Mathlib plus the MathFin library for Girsanov, generated by an AI system.
Abstract
This is an expository note on the asymptotics of the Wasserstein distance between the empirical measure of infinite-dimensional random paths and their common distribution. We present the classical proof for these asymptotics in the case of the Wiener measure, unifying quantization arguments from Dereich and coauthors or Boissard and Le Gouic, and we adapt it for Itô diffusions sampled through the Girsanov theorem. More precisely, let $\mathbb{Q}$ be the law of the solution of a stochastic differential equation with a bounded Lipschitz drift. Let $W_1,\ldots,W_n$ be independent Brownian paths, and let $Z_i$ be their Girsanov weights for $\mathbb{Q}$. The reweighted empirical measure $$\widehatμ_n=\frac{\sum_{i=1}^n Z_iδ_{W_i}}{\sum_{i=1}^n Z_i}$$ approximates $\mathbb{Q}$ when $n$ is large. We prove that the Wasserstein cost $W_p^p(\widehatμ_n,\mathbb{Q})$ is of order $(\log n)^{-p/2}$, in expectation and almost surely, for every fixed $p\geqslant1$. In the Brownian case where $Z_i=1$ these results show that $\sqrt{\log n}W_p(\widehatμ_n,\mathbb{Q})$ is asymptotically sandwiched between $\sqrt{2λ_d}$ and $4\sqrt{2λ_d}$, where $λ_d$ is the first eigenvalue of the Laplacian operator in the unit ball. We provide numerical experiments to estimate the (conjectured) limiting constant in dimension $d=1$.
Problem
The note studies how fast the Wasserstein distance between the empirical measure of n random paths and their common law decays. It covers Brownian (Wiener) paths and Itô diffusions sampled by Girsanov reweighting of Brownian paths.
Approach
Classical Wiener quantization arguments of Dereich et al. and Boissard–Le Gouic are unified using small-ball probabilities and Anderson's inequality. The argument is then adapted to the self-normalized Girsanov-weighted empirical measure for SDEs with bounded Lipschitz drift, using moment controls on the weights. The results are formalized in Lean 4, relying on the MathFin library because Mathlib lacks stochastic calculus. The formalization was produced by an AI system and audited for concordance with the paper by AI systems.
Results
The Wasserstein cost W_p^p is of order (log n)^{-p/2}, in expectation and almost surely, for every p ≥ 1. In the Brownian case, sqrt(log n)·W_p is asymptotically between sqrt(2λ_d) and 4·sqrt(2λ_d), where λ_d is the first eigenvalue of the Laplacian in the unit ball. Numerical experiments estimate the conjectured limiting constant in dimension d=1.
