Modeling Fo-Limits for Monadically Stable Sequences

We show that given a monadically stable theory T, a sufficiently saturated M T, and a coherent system of probability measures on the $σ$-algebras generated by parameter-definable sets of M in each dimension, we may produce a totally Borel B M realizing these measures. Our main application is to prove that every FO-convergent sequence of structures (with countable signature) from a monadically stable class admits a modeling limit. As another consequence, we prove a Borel removal lemma for monadically stable Lebesgue relational structures.