{"id":"palomar/PALOMAR-2026-10-15-000007","url":"https://github.com/sascha2718/lean-brownian-images/tree/343d25c53699fbcb2372d3016002993d475e249e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000007-v1.json","repo":"https://github.com/sascha2718/lean-brownian-images","tags":["math.PR","math.DS","msc:60J65","msc:28A80","stochastic-processes","brownian-motion","fractal-measures"],"score":0,"title":"Distinguishing sets and measures from their planar Brownian images","trust":"high","domain":"math.PR","source":"palomar","authors":["Sascha Troscheit"],"reviews":0,"subject":"math.PR","summary":"Lean 4 formalisation of all 32 numbered statements of \"Distinguishing sets and measures from their planar Brownian images\" (Sascha Troscheit, arXiv:2610.16339), which asks whether two deterministic time measures on the unit interval can be distinguished almost surely from a single planar Brownian image. Rescaled correlation integrals of the time measures determine expected correlation profiles of the image measures, and profiles that differ in the limit make the image laws mutually singular, even when the time measures have the same dimension. For natural measures of self-similar sets…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Distinguishing sets and measures from their planar Brownian images","identifier":"https://arxiv.org/abs/2610.16339","relationship":"formalizes"}]}