{"id":"palomar/PALOMAR-2026-11-02-000008","url":"https://github.com/zblore/kac-lean/tree/bfeb867d5a9b469cb11139c296e9bd41706e0992","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-02-000008-v1.json","repo":"https://github.com/zblore/kac-lean","tags":["math.DS","msc:37A05","msc:37A40","msc:28D05"],"score":0,"title":"Kac's return-time formula for any measure-preserving map","trust":"high","domain":"math.DS","source":"palomar","authors":["Zayn Blore"],"reviews":0,"subject":"math.DS","summary":"A machine-checked proof of Kac's return-time formula. For a measure-preserving map f and a measurable set A, the integral over A of the first return time to A equals the measure of the points whose orbit ever meets A. The return time is valued in the extended naturals, infinite for a point that never returns, and with that convention the formula holds for every measure, with no finiteness, sigma-finiteness, conservativity or ergodicity assumption. For an ergodic map of a probability space and mu(A) > 0 the integral is 1, so the mean return time to A, starting in A, is 1 / mu(A).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-02","reactions":{},"formalized":true,"formalizes":[{"title":"On the spatial mean of the Poincaré cycle","identifier":"https://arxiv.org/abs/math/0505625","relationship":"adapts"}]}