Commit 2026-10-13 16:28 db57686d

refactor(MeasureTheory/Function): generalize Egorov's theorem (#44804) This PR adapts Egorov's theorem to AEStronglyMeasurable functions and NullMeasurable sets. There is no clear generalization of tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist or tendstoUniformlyOn_of_ae_tendsto, so I kept the old measurable version and gave an a.e. measurable version. This modification simplifies the applications of Egorov's theorem, and avoids a couple of painful reductions to measurable settings.