Commit 2026-09-25 23:29 b2bf0519

chore(MeasureTheory): generalize hypotheses to NullMeasurableSet (#42924) This PR generalizes many statements in Mathlib.MeasureTheory from MeasurableSet s to NullMeasurableSet s μ. This is particularly useful for lemmas around uniform integrability. A few technical statements which existed only to work around issues of measurability are deprecated thanks to this: MemLp.eLpNorm_indicator_le_of_meas, UniformIntegrable.spec', MemLp.uniformIntegrable_of_identDistrib_aux. This PR is a preliminary (and necessary) work before a much more thorough refactor of MeasureTheory.Function.UniformIntegrable. I have chosen to change the hypotheses in place (generalizing the lemmas) instead of adding variants with the new hypothesis, in order to limit quasi-duplicates. There are some limits to this strategy, and a few lemmas have now both MeasurableSet and NullMeasurableSet versions:

• either if the MeasurableSet version was tagged as simp;
• or integrable_indicator_iff₀, setLIntegral_congr_fun_ae₀, setLIntegral_congr_fun₀, setLIntegral_eq_zero₀, lintegral_add_compl₀, setLIntegral_compl₀. The latter 6 lemmas account for the largest potential downstream effects of this PR. If I did not keep the former versions of these 6 lemmas, this PR would have affected five time as many files, including files in e.g. Geometry or NumberTheory. It seems reasonable that, for quality of life purposes, we keep a few files with MeasurableSet hypotheses which are widely used in settings where measurability is essentially a given. Edit: Implementation note: Some lemmas (e.g. UniformIntegrable.spec) were previously proved in two steps. First a version for Measurable/StronglyMeasurable functions (in this instance, this is lemma UniformIntegrable.spec'), then a weakening of the measurability hypotheses. This PR makes it convenient to prove directly the more general version of these lemmas. In these case, I have put the more general lemmas (UniformIntegrable.spec) before, deduced the weaker version (UniformIntegrable.spec') from it, and deprecated the latter. This strategy, however, makes the git diff somewhat annoying to read.