Commit 2022-07-25 14:27 287a69a0

refactor(measure_theory/function/uniform_integrable): change uniform_integrable to only require ae_strongly_measurable (#15623) The L¹ version of the strong LLN does not require strongly_measurable but the assumption in uniform_integrable forces it to have this condition if not requiring an extra step to relax the condition (see #15392). This PR relaxes the definition of uniform_integrable so it only requires ae_strongly_measurable.