Commit 2025-01-03 14:42 478f8eac

chore: use unsigned measures for Lebesgue decomposition (#20400) Signed measures require around 500 more imports than unsigned measures, because they use Bochner integration. As there is no particular reason to use signed measures to prove the Lebesgue decomposition theorem, we use unsigned measures instead. This PR does not have a big impact on imports, since the file also contains other lemmas about integrability. The effect will be seen in a future PR splitting those out.