Commit 2025-04-15 05:27 67b4128e

chore: split MeasureTheory.Integral.Lebesgue.Basic (#23860)

• .Add contains some versions of the monotone convergence theorem, Fatou's lemma and addition and constant multiplication of integrals.
• .Sub contains subtraction of integrals and more versions of monotone convergence (in particular those versions operating on antitone sequences of functions).
• .Markov contains Markov's inequality and lemmas that depend on it.
• .DominatedConvergence contains the dominated convergence theorem.
• Results on maps of measures have been moved to .MeasurePreserving, which already deals with measure-preserving maps. Since the scope has broadened, the file has been renamed to .Map.