Sharp Wasserstein propagation of chaos from correlated initial data
A Lean 4 proof, checked against Mathlib, of a sharp quantitative propagation of chaos estimate for mean field diffusions dX_i = (a(X_i) + N^{-1} sum_j K(X_i, X_j)) dt + sqrt 2 dW_i with a globally Lipschitz one-body drift a and a bounded, globally Lipschitz pairwise interaction K. If every k-particle marginal of the (possibly correlated and singular) exchangeable initial law lies within squared quadratic Wasserstein distance C_0 (k/N)^2 of the corresponding power of the McKean-Vlasov initial law, then the same holds on every finite time interval [0, T] with an explicit constant C_T that…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-08-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-08-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-08-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'