The proof of lemma unif_integrable_of_tendsto_Lp did essentially the following:

• write f as g + (f - g) and say that f was unif_integrable as sum of unif_integrable functions
• state that g was unif integrable since it's a single function in Lp
• prove that if a sequence f of Lp tends to 0 in snorm, then it is unif_integrable

I cut the lemma in several pieces and added unif_integrable.add, unif_integrable.neg, unif_integrable.sub, unif_integrable_const. Overall, the proof of unif_integrable_of_tendsto_Lp was a bit long because you did not develop enough API about your new definition.

Please review my commit and change anything you don't like!

Thanks a lot! The changes look great

I added congr_ae lemmas for unif_integrable and used them to remove measurability assumptions from Vitali's convergence theorem.

This PR is now looking quite good, but I have an issue with the names. IMany different lemmas have the name snorm_indicator_ge_le and small variations on that. Can you make those more distinct?

Among all those results, some lemmas prove the existence of an M and use sets where the norm is large and others prove the existence of a delta and use any sets with measure less than delta. The names should in particular reflect that difference.

I've changed the names of the lemmas now and added some doc string. Hopefully, it is more clear now.

Thanks ! Those names are good.
bors r+

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests