Commit 2026-03-09 13:45 9d0ea7dd

feat: integrability with respect to a countable sum of measures (#36355) Create a new file to prove that Integrable f (Measure.sum μ) ↔ (∀ i, Integrable f (μ i)) ∧ Summable (fun i ↦ ∫ x, ‖f x‖ ∂μ i) and specialize this for sums of Dirac masses. Also move existing results about integrals against sums of measures to the new file.