{"id":"palomar/PALOMAR-2026-10-08-000001","url":"https://github.com/yuhaolei-ctrl/Sharp-W2-to-W2-Propagation-of-Chaos/tree/84dbe881384ad2f0358857b025ef6fd824ebc9a1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-08-000001-v1.json","repo":"https://github.com/yuhaolei-ctrl/Sharp-W2-to-W2-Propagation-of-Chaos","tags":["math.PR","msc:60K35","msc:82C22","msc:60H10","msc:35Q84","msc:49Q22","propagation-of-chaos","mean-field-diffusions","lean-formalization"],"score":0,"title":"Sharp Wasserstein propagation of chaos from correlated initial data","trust":"high","domain":"math.PR","source":"palomar","authors":["Yuhao Lei"],"reviews":0,"subject":"math.PR","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-08","reactions":{},"formalized":true,"formalizes":[{"title":"Sharp Wasserstein propagation of chaos from correlated initial data","identifier":"","relationship":"formalizes"}]}